digama0
I'm a post-doc working on formal mathematics and interactive theorem proving. I am an expert in the Metamath and Lean proof languages.
Carnegie Mellon University
Pinned Repositories
frat
DRAT proof processor
lean-sys
Rust bindings for the Lean 4 proof assistant
lean-type-theory
LaTeX code for a paper on lean's type theory
lean4lean
Lean 4 kernel / 'external checker' written in Lean 4
mizar-rs
Alternative Mizar proof checker (http://mizar.org/) written in Rust
mm-lean4
Lean 4 Metamath verifier
mm0
Metamath Zero specification language
mmj2
mmj2 GUI Proof Assistant for the Metamath project
olean-rs
parser/viewer for olean files (lean 3)
mathlib
Lean 3's obsolete mathematical components library: please use mathlib4
digama0's Repositories
digama0/mm0
Metamath Zero specification language
digama0/mmj2
mmj2 GUI Proof Assistant for the Metamath project
digama0/lean4lean
Lean 4 kernel / 'external checker' written in Lean 4
digama0/mizar-rs
Alternative Mizar proof checker (http://mizar.org/) written in Rust
digama0/mm-lean4
Lean 4 Metamath verifier
digama0/frat
DRAT proof processor
digama0/lean-sys
Rust bindings for the Lean 4 proof assistant
digama0/lean-rs
High level Lean 4 FFI for Rust
digama0/dtt.mm
Metamath database for dependent type theory
digama0/mm-web-rs
A metamath web site generator in rust
digama0/leangz
Lean 4 .olean file (de)compressor
digama0/lean-cache
Lean 4 build cache management tool
digama0/coq-rs
A Coq .vo parser in Rust
digama0/lafny
Some experiments in Dafny-like syntax in Lean 4
digama0/oleandump
A type-aware olean tparser for Lean 4 olean files
digama0/digama0.github.io
My personal website
digama0/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
digama0/lean4checker
Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
digama0/minidom-14
digama0/verbose-lean4
Natural language tactics to teach mathematics using Lean 4
digama0/bors-ng
👁 A merge bot for GitHub Pull Requests
digama0/doc-gen4
Document Generator for Lean 4
digama0/lean4
Lean 4 programming language and theorem prover
digama0/lean4-zig
Zig bindings for Lean4
digama0/LeanColls
WIP collections library for Lean 4
digama0/LeanSAT
digama0/mizar-system
digama0/moonrider
🌕🏄🏿 Surf the musical road among the stars. Side project built by two people in a few months to demonstrate WebXR.
digama0/rust-clippy
A bunch of lints to catch common mistakes and improve your Rust code. Book: https://doc.rust-lang.org/clippy/
digama0/vscode-lean4
Visual Studio Code extension for the Lean 4 proof assistant