Pinned Repositories
mr2bib
greek_enumerate
Greek letters for enumerates in LaTeX (depends on the enumitem package)
mtcaxa
The Mumford–Tate conjecture for products of abelian varieties
lean-liquid
💧 Liquid Tensor Experiment
lean-perfectoid-spaces
Perfectoid spaces in the Lean formal theorem prover.
mathlib3
Lean 3's obsolete mathematical components library: please use mathlib4
jcommelin's Repositories
jcommelin/mtcaxa
The Mumford–Tate conjecture for products of abelian varieties
jcommelin/queueboard
Mathlib4 review and triage dashboard
jcommelin/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
jcommelin/Diagram-chasing
The code produced during my internship at the Math Institute of Freiburg (under the supervision of Johan Commelin)
jcommelin/elan
A Lean version manager
jcommelin/glimpse_of_lean
An introduction to theorem proving in Lean for the impatient.
jcommelin/HoTT
Homotopy type theory
jcommelin/informal-formalization-seminar
jcommelin/lean-ctt-snapshot
jcommelin/lean.nvim
neovim support for the Lean theorem prover
jcommelin/lean4
Lean4 work in progress repo
jcommelin/lean4-metaprogramming-book
jcommelin/lean4-nightly
Nightly builds
jcommelin/leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.
jcommelin/leanprover-contrib
jcommelin/mathematics_in_lean_source
Source code for the Mathematics in Lean tutorial.
jcommelin/mathlib
Lean mathematical components library
jcommelin/maze-game
An abstraction of a maze.
jcommelin/mm0
Metamath Zero specification language
jcommelin/nixpkgs
Nix Packages collection & NixOS
jcommelin/oberharmersbach_2021
jcommelin/pila_wilkie_seminar
jcommelin/primes-and-crypto
Workshop on prime numbers and cryptography
jcommelin/pygments
Pygments is a generic syntax highlighter written in Python
jcommelin/rubiks-solver-ai
jcommelin/sd-nix
some helpers for working with nix
jcommelin/sembreak
jcommelin/stacks-project
Repository for the Stacks Project
jcommelin/verbose-lean4
Natural language tactics to teach mathematics using Lean 4
jcommelin/vscode-lean
An extension for VS Code which provides support for the Lean language.