Patrick Massot

GlimpseOfLean. An introduction to theorem proving in Lean for the impatient.

leanblueprint. plasTeX plugin to build formalization blueprints.

verbose-lean4. Natural language tactics to teach mathematics using Lean 4

lean-verbose. Very controlled natural language tactics for Lean

lean-differential-topology. This may become a formalization of smooth manifolds in lean

lean4-game-server. Lean

NNG4. Lean

tikzcdedit. Small javascript frontend to tikz-cd

MDD154. Lean

plastexdepgraph. Dependency graph plugin for plasTeX

proofs_with_lean. An introduction to proofs with Lean using controled natural language

GaloisConnectionGame. Lean

lean-gym. Lean

checkdecls. Tiny Lean library to check existence of declarations

lean-scratchpad. Experimentation with the Lean prover

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

zmk-keyboard-quacken. C

lean-lsp-experiments.nvim. Lua

ngram-type-fr. A French version of the Ngram-Type Touch typing trainer. Uses French n-grams as a data source.

math2001. Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

exeterDemo. Lean

lean-bavard. Lean

verbose_lean_manual. Lean

bigop. Lean port of the mathcomp big operators lib