Lean is a functional programming language that makes it easy to write correct
and maintainable code. You can also use Lean as an interactive theorem prover.
Lean programming primarily involves defining types and functions. This allows
your focus to remain on the problem domain and manipulating its data, rather
than the details of programming.
📐 Natural language explanations of Lean 4 theorems | MathJax 4.0 rendering • Batch processing • Mathematical notation | Formal verification accessibility
An AI proof pipeline whose only judge is the Lean compiler. A file whose proof is 'sorry' compiles and exits 0 - so certification here means: compiles, no cheat rules, kernel axiom report clean, statement untouched by the model.
Research code and Lean infrastructure for studying when drifting fields identify their target distributions.
Reproduction of Ax-Prover: a 3-agent LLM framework for automated Lean 4 theorem proving
Computer-assisted proof and reproducibility package for Erdős Problem 848, with exact certificates and separately implemented checkers.
Uniform spectral gap for the Syracuse (3n+1) mod-2^k transfer operator, proved elementarily for all scales (cert <= 0.8536). The earlier cycle-elimination claim is retracted (3x-1 control) - see README/THEOREM.md. Not a proof of Collatz.
A local prototype for verifier-guided multi-round Lean proof search with Hermes as solver and Codex as host orchestrator
Staged research package for Fibonacci-anyon topological quantum computing, SHA-520 boundary analysis, and proof-directed search.
Verification-first autonomous research orchestrator with Lean-checked proofs, resumable human handoffs, and evidence provenance.
Automated neuro-symbolic pipeline classifying Calabi-Yau periods — exact Q-nullspace algebraic shielding, 0-axiom Lean 4 formal verification, and Callens-ALIX INT64 attention kernels.
Can a machine recover mathematical structure from an anonymized formal theory and a proof checker alone?
A formal logic theorem prover, formula explorer, deducer, and Lean 4 exporter in Python with Cython acceleration.
Turn formally verified Lean 4 proofs into cinematic, semantically animated videos.
A witness-governed research stack bridging analogue, digital, and formal systems through Self Referential Neural Network(SRNN) cognition, evidence contracts, and reference runtimes.
A maintained catalog of public repositories that machine-check quantum programs, circuits, protocols, and error correction in proof assistants — with the proof system, what each verifies, and a dated build observation.
Command line tool to help improve the quality of Lean code by converting any "simp" to "simp only".
Collapse System Logic — deterministic proof collapse (E→Z→1)
Pisa is a Django website for teachers to design and assign programming and proof assignments in Lean4, Microsoft's open-source proof assistant
Created by Leonardo de Moura
Released 2013