Kimina Lean Server

Stream: Machine Learning for Theorem Proving

[Marco Dos Santos]

The Kimina Team recently released Kimina-Prover Preview, achieving SOTA on miniF2F. Yesterday, we released a demo of our 72B model.

Today, we’re open-sourcing the Kimina Lean Server, which we used to train Kimina-Prover!
It enables fast and scalable interaction with Lean 4 via a unified REST API, and is designed as a simple verifier for reinforcement learning pipelines.
It supports:

• Large-scale verification
• Proof data extraction
• Interaction

We'd love to hear your feedback!

Code: https://github.com/project-numina/kimina-lean-server
Technical report: https://github.com/project-numina/kimina-lean-server/blob/main/Technical_Report.pdf

[Kelly Davis]

In case anyone is interested, as an enhancement to kimina-lean-server I added two add Abstract Syntax Tree (AST) endpoints using ast_export.

The AST version is in the fork kimina-lean-server and seems to work.

The major limitation is that if one wants to create an AST for code, then the modules that code uses must be a dependency of ast_export, e.g. if code were allowed to depend on mathlib, the lakefile.lean of ast_export would contain the line

...
require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
...

In my implementation I only need a Mathlib4 dependency. So that's all that's pulled in.

Generation of an AST for arbitrary code would require modifications.