jcommelin Goto Github PK

batteries

The "batteries included" extended library for the Lean programming language and theorem prover

berkovich

Lecture notes of the workshop on Berkovich skeleta

csskeyboard

CSS keyboard keys

diagram-chasing

The code produced during my internship at the Math Institute of Freiburg (under the supervision of Johan Commelin)

elan

A Lean version manager

glimpse_of_lean

An introduction to theorem proving in Lean for the impatient.

greek_enumerate

Greek letters for enumerates in LaTeX (depends on the enumitem package)

groupreps

Candidate groups for a given representation

hott

Homotopy type theory

informal-formalization-seminar

lean

lean-ctt-snapshot

lean-homotopy-theory

A development of homotopy theory in the Lean formal theorem prover.

lean-perfectoid-spaces

A formalization of the concept of a perfectoid space in the Lean formal theorem prover.

lean-tidy

lean.nvim

neovim support for the Lean theorem prover

lean4

Lean4 work in progress repo

lean4-metaprogramming-book

leanprover-contrib

lt2019_slides

Sheaves and Lean — Lean Together 2019

mathematics_in_lean_source

Source code for the Mathematics in Lean tutorial.

mathlib

Lean mathematical components library

maze-game

An abstraction of a maze.

mm0

Metamath Zero specification language

morphism

Typesetting morphisms in LaTeX

mtcaxa

The Mumford–Tate conjecture for products of abelian varieties

oberharmersbach2019

oberharmersbach_2021

ograv

On ordinary good reduction of abelian varieties

pila_wilkie_seminar