The Lean research ecosystem, in one directory.

Formalization of Moreira's version of Sard's Theorem

Lean formalisation of the classification of the groups of order p * q where p and q are prime numbers.

Formalization of Frucht's theorem in Lean

GitHub repository for the seminar on Computer-assisted mathematics held at the University of Heidelberg during the Summer Semester of 2024.

Formalization of Markov Chain Monte Carlo in Lean 4

A formalisation of the disproof of Ramaekers's conjecture

Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.

A Lean4 Formalization of Fibred Categories

Formalisation of mean Fourier analysis in Lean 4

A formalisation of the Selberg sieve in Lean 4

Official implementation of "FLARE: Verifying MILP Reformulations with LLM-Based Formal Proof Synthesis"

A formalized proof of Artin-Wedderburn theorem in Lean4

Proof of Lean: Formalizing Blockchain Fundamentals in Lean

Lean code formalizing a proof of Legendre's theorem on diagonal ternary quadratic forms

Perron-Frobenius, Jentzsch theorem, and matrix/operator positivity in Lean 4

Formalization of a new data structure: Dashed-Monoids

Lean 4 formalization of finite Bayes-threshold optimality for OrdVec overlap models.

Formalization in Lean of the transcendence of π.