Skip to content

p135246/computational-research

v0.1.0MIT

Wolfram-centric computational research: organize projects and sources, maintain a wiki, create and edit notebooks, collaborate on human-owned papers and paclet designs through concise notes companions, develop and publish paclets, retrieve citations, formalize requested proofs, and manage a backlog with isolated workers. Preserves human edits and author-controlled iterations; publication requires an explicit request. README.md is the authoritative workflow blueprint.

paper-lean

Drive a Lean 4 / Mathlib formalization session via the lean-lsp MCP. Opens a file, reads the goal state, searches Mathlib for closing lemmas, verifies proofs, and writes a formalization checklist to Work/. Use when the user says "formalize in Lean", "prove this in Lean", "what's the Mathlib name for X", "check this Lean proof", "lean state", or during math-research projects with a Lean/ subdirectory.

Read SKILL.md at the source

Pinned to revision a6ba23e0db02, so it is the text this page describes rather than whatever the author pushed since.

Files

Every link opens the file at its source, pinned to the revision this page describes.