Pinned Repositories
GlimpseOfLean
An introduction to theorem proving in Lean for the impatient.
lean-differential-topology
This may become a formalization of smooth manifolds in lean
lean-perfectoid-spaces
A formalization of the concept of a perfectoid space in the Lean formal theorem prover.
lean-verbose
Very controlled natural language tactics for Lean
lean4-game-server
leanblueprint
plasTeX plugin to build formalization blueprints.
NNG4
plastex
Python package to convert LaTeX markup to DOM
tikzcdedit
Small javascript frontend to tikz-cd
verbose-lean4
Natural language tactics to teach mathematics using Lean 4
PatrickMassot's Repositories
PatrickMassot/leanblueprint
plasTeX plugin to build formalization blueprints.
PatrickMassot/GlimpseOfLean
An introduction to theorem proving in Lean for the impatient.
PatrickMassot/verbose-lean4
Natural language tactics to teach mathematics using Lean 4
PatrickMassot/lean-verbose
Very controlled natural language tactics for Lean
PatrickMassot/checkdecls
Tiny Lean library to check existence of declarations
PatrickMassot/exeterDemo
PatrickMassot/math2001
Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
PatrickMassot/MDD154
PatrickMassot/ngram-type-fr
A French version of the Ngram-Type Touch typing trainer. Uses French n-grams as a data source.
PatrickMassot/plastexdepgraph
Dependency graph plugin for plasTeX
PatrickMassot/arsenik
A 33-key layout that works with all keyboards.
PatrickMassot/bptest
PatrickMassot/GitPython
GitPython is a python library used to interact with Git repositories.
PatrickMassot/kalamine
Keyboard Layout Maker
PatrickMassot/lean4
Lean 4 programming language and theorem prover
PatrickMassot/leanprover.github.io
www
PatrickMassot/LspExperiments
PatrickMassot/M2Yannis
PatrickMassot/monaspace
An innovative superfamily of fonts for code
PatrickMassot/neovim_config
PatrickMassot/pfr
PatrickMassot/plastexshowmore
Show more plugin for plasTeX
PatrickMassot/private
Dotclear 2 plugin
PatrickMassot/ProofWidgets4
Helper toolkit for creating your own Lean 4 UserWidgets
PatrickMassot/std4
Standard Library for Lean 4
PatrickMassot/symmetric_project
PatrickMassot/testing-lower-bounds
Lower bounds on testing and estimation, in Lean
PatrickMassot/vi-xournalpp
A small plugin for Xournal++ version 1.1.x and 1.2.x with vi-like modes
PatrickMassot/Whitney-Graustein-Formalization
PatrickMassot/zmk-config