Skip to content
Published studies are shown for demonstration purposes, not because they are good or bad research. Demonstrator · items marked Example are invented · what exists today
Search

Skills · Theorist Toolbox

agent:lean-prover

By Moran Koren · as credited by the source

Formalises a lemma in Lean 4 and verifies it with lake build — a green build is the strongest "proven" the system supports; the reviewer re-runs the build rather than re-checking the mathematics.

In the catalogue
No evaluations yet
Anyone can contribute. Improve this skill Contribute a skill

Provenance

Project
Theorist Toolbox
Maintained by
Moran Koren (Ben-Gurion University of the Negev, Economics)
Licence
MIT · can be redistributed
Source file
morankor/theorist-toolbox/blob/main/agents/lean-prover.md
Identifier
theorist-toolbox/lean-prover

Use it

e2er skills install theorist-toolbox

The command is in e2er 0.10.0 and later.

Cite this skill
Persistent identifiers planned 
@software{morankorenbengurionunive2026agentleanprover,
  title   = {agent:lean-prover},
  author  = {Moran Koren (Ben-Gurion University of the Negev, Economics)},
  year    = {2026},
  note    = {e2er skill. Persistent identifier planned},
  url     = {https://github.com/morankor/theorist-toolbox/blob/main/agents/lean-prover.md}
}
 Report a failure

Used by

No e2er specialist loads this skill by default. Once installed, a template can assign it to a specialist.

Description

Data model
Discipline
General
Method family
not specified
Design
not specified
Research stage
Formal modeling
Authors
Moran Koren
Usage
not used in published research yet
Source
RISE skill catalogue · theorist-toolbox · @4c17bae
Record
skill:theorist-toolbox/lean-prover · JSON

Solid tags are declared by the source or mapped from its terms; dashed tags are inferred by a published rule. Hover a tag for its provenance.

More

auditMIT

Evaluations

Planned

No evaluation record yet. An evaluation shows where a skill breaks before others rely on it.

Evaluate this skill

More audit skills in Theorist Toolbox

/codex-math

On e2er.org

Loading…

Report a failurePropose a new version

Discussion

Loading…