Mario Carneiro

mm0. Metamath Zero specification language

lean4lean. Lean 4 kernel / 'external checker' written in Lean 4

lean-type-theory. LaTeX code for a paper on lean's type theory

mmj2. mmj2 GUI Proof Assistant for the Metamath project

mizar-rs. Alternative Mizar proof checker (http://mizar.org/) written in Rust

lean-sys. Rust bindings for the Lean 4 proof assistant

mm-lean4. Lean 4 Metamath verifier

ast_export. AST export from Lean 4

frat. DRAT proof processor

tpil25. Course materials for Chalmers TPIL25 class

lean-rs. High level Lean 4 FFI for Rust

olean-rs. parser/viewer for olean files (lean 3)

mm-hammer. A tool for automatically proving Metamath theorems using ATPs

leangz. Lean 4 .olean file (de)compressor

dae-parser. Rust crate for parsing Collada DAE files

MCRedstoneSim. Baezon's Redstone Simulator

advent-of-code. The Advent of Code programming puzzles in Lean

oleandump. A type-aware olean tparser for Lean 4 olean files

dtt.mm. Metamath database for dependent type theory

vc0. C0 specification and verified compiler in Lean

mm-web-rs. A metamath web site generator in rust

mm-scala. A Metamath verifier in Scala

lean-cache. Lean 4 build cache management tool

FLT. Ongoing Lean formalisation of the proof of Fermat's Last Theorem

twitchcoq. It's a poorly named metamath verifier

mathlib-ITP2019. mathlib library, prepared for the paper "Formalizing computability theory via partial recursive functions"

lafny. Some experiments in Dafny-like syntax in Lean 4

asm_simulator. Java

coq-rs. A Coq .vo parser in Rust

isabelle-rs. Parser for isabelle database files

hol4-vscode. HOL4 mode for VSCode

LeanSAT. Lean