My personal repository of formally verified mathematics.
A template for blueprint-driven formalization projects in Lean.
Riemann Hypothesis in Lean
Experiments with interactive theorem provers, LLMs and formal systems
Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.
Lean project for Fall 2020
Lean 4 multi-target compiler: one portable program source → EVM, Solana, NEAR, Noir with fail-closed semantics (proof-forge-next)
a Lean implementation of Jensen's Inequality
Used to store short program examples
Learning how to use the Lean theorem prover
OPEN GATE, a 512-byte, 150-µs hot-patch gatekeeper that treats every Latin letter as a thermodynamic token whose semantic load Λ(ℓ) = log2(pcorpus/pconcept) is a conserved quantity.
Formalization experiments around structural behavior near critical points of arithmetic functions.
Add a description, image, and links to the lean-theorem-prover topic page so that developers can more easily learn about it.
To associate your repository with the lean-theorem-prover topic, visit your repo's landing page and select "manage topics."