Paper | Leandex | Demo | Putnam 2025 An agent built on Claude Code for formal theorem proving tasks. We used this system to prove all 12 problems from Putnam 2025, and completed a paper-level formalization of Effective Brascamp-Lieb inequalities.
@project-numinaCode transformation tools for repairing, simplifying, and extracting Lean proofs
@project-numinaLLM-assisted tools for informal proofs, proof strategy discussion, and code simplification
@project-numinaSearch tools for finding Lean theorems, lemmas, and definitions in Mathlib
@project-numinaIsolates failing proof steps by replacing them with `sorry` and extracting them into standalone lemmas to modularize and decouple…
@project-numinaVerification tools for compiling, validating, and disproving Lean theorems
@project-numina© 2026 Flowy
Built for Claude Code · Not affiliated with Anthropic
