Numina-Lean-Agent

A mathematical agent combining a coding assistant with Lean feedback, theorem search and reasoning tools.

• Developer / Organization: Project Numina; Junqi Liu and collaborators
• Category: Open-source formalization & proving
• Purpose: Use general-purpose coding agents for formal mathematical reasoning.
• Key features: A Claude Code-based agent combining Lean feedback, theorem search and auxiliary reasoning tools.
• Availability: Open-source software; MIT (stated in README)
• License: MIT (stated in README) (source (opens in a new tab))
• Website / Source code: https://github.com/project-numina/numina-lean-agent (opens in a new tab)
• Version: Source package: 0.1.0 (not a GitHub release)
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01