Johan Commelin
jcommelin
Languages
Repos
60
Stars
8
Forks
0
Top Language
Lean
Loading contributions...
Top Repositories
Repositories
60No description provided.
No description provided.
No description provided.
No description provided.
No description provided.
The Mumford–Tate conjecture for products of abelian varieties
An introduction to theorem proving in Lean for the impatient.
The math library of Lean 4
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
No description provided.
Basic Unicode support for Lean 4
computable implementation of real numbers in Lean4
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
The "batteries included" extended library for the Lean programming language and theorem prover
No description provided.
some helpers for working with nix
Pygments is a generic syntax highlighter written in Python
Nix Packages collection & NixOS
Hosts the website for mathlib and other Lean community infrastructure.
Natural language tactics to teach mathematics using Lean 4
Nightly builds
Greek letters for enumerates in LaTeX (depends on the enumitem package)
No description provided.
No description provided.
No description provided.
Lean mathematical components library
No description provided.
Workshop on prime numbers and cryptography
The code produced during my internship at the Math Institute of Freiburg (under the supervision of Johan Commelin)
neovim support for the Lean theorem prover