Stars
Github repository about formalization of formal group laws.
These are the lecture notes for the course "Logic of Proof Assistants" taught in Bonn in the summer term 2025 by Prof. van Doorn.
Transformers for Mathematics Tutorial | Simons/SLMath Workshop on AI for Mathematics 2025
Formalizing some theorems about Demazure operators in Lean4
Goldbach conjecture = 25-state turing machine
In this repository I am collecting the code of my formalisation of CW complexes in Lean.
Formalisations for simplicial HoTT and synthetic ∞-categories.
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
The "batteries included" extended library for the Lean programming language and theorem prover
A project to map out the relations between different equational theories of Magmas.
A formal proof of the independence of the continuum hypothesis
Draft proposal for additional sub/superscript characters in Unicode
Predicts the amount of resources spent and gained by each action in the action list.
A work in progress proof checker for LRAT files written in Lean.
Tactics for discharging Lean goals into SMT solvers.
Emacs major mode for Lean 4
Type Lean unicode characters in your web browser