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.

Chalmers University of TechnologyGothenburg, Sweden

Pinned Repositories

frat
DRAT proof processor
Language:Rust13 4 153
lean-rs
High level Lean 4 FFI for Rust
Language:Rust13 2 01
lean-sys
Rust bindings for the Lean 4 proof assistant
Language:Rust19 3 26
lean-type-theory
LaTeX code for a paper on lean's type theory
Language:TeX129 6 15
lean4lean
Lean 4 kernel / 'external checker' written in Lean 4
Language:Lean97 6 18
mizar-rs
Alternative Mizar proof checker (http://mizar.org/) written in Rust
Language:Rust50 6 113
mm-lean4
Lean 4 Metamath verifier
Language:Lean17 5 01
mm0
Metamath Zero specification language
Language:Lean334 21 5841
mmj2
mmj2 GUI Proof Assistant for the Metamath project
Language:Java74 11 3926
mathlib4
The math library of Lean 4
Language:Lean1.7k 37 441372

digama0's Repositories

digama0/lean-type-theory
LaTeX code for a paper on lean's type theory
Language:TeX129 6 15
digama0/mm-lean4
Lean 4 Metamath verifier
Language:Lean17 5 01
digama0/frat
DRAT proof processor
Language:Rust13 4 153
digama0/dae-parser
Rust crate for parsing Collada DAE files
Language:Rust10 3 20
digama0/mm-hammer
A tool for automatically proving Metamath theorems using ATPs
Language:Rust10 4 02
digama0/dtt.mm
Metamath database for dependent type theory
Language:Objective-C++5 5 12
digama0/lafny
Some experiments in Dafny-like syntax in Lean 4
Language:Lean2 2 0
digama0/a-mir-formality
a PLT redex model of MIR and its type system
Language:Racket0 0
digama0/cadical
CaDiCaL SAT Solver
Language:C++2 02
digama0/CMark.lean
Language:C0 0
digama0/glium
Safe OpenGL wrapper for the Rust language.
digama0/gltf-rs
A crate for loading glTF 2.0
Language:Rust0 0
digama0/hz-to-mm0
HOL Zero to Metamath Zero translator
Language:Rust3 01
digama0/if_chain
Macro for writing nested `if let` expressions
Language:Rust2 0
digama0/lake
Lean 4 build system and package manager with configuration files written in Lean.
Language:Lean1 0
digama0/lean-1
Lean Theorem Prover
Language:C++1 0
digama0/lean3port
Stub for downloading mathport artifacts for Lean 3
digama0/lean4-cli
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
Language:Lean0 0
digama0/LeanInk
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Language:Lean0 0
digama0/metamath-syntax-highlighting
digama0/minisat
A minimalistic and high-performance SAT solver
Language:C++1 1
digama0/mizar-system
Language:Pascal1 0
digama0/pof-tools
Program for manipulating the Freespace model format .pof
Language:Rust0 0
digama0/quote4
Intuitive, type-safe expression quotations for Lean 4.
Language:Lean0 0
digama0/rust
Empowering everyone to build reliable and efficient software.
Language:Rust2 0
digama0/rust-analyzer
A Rust compiler front-end for IDEs
digama0/team
Rust teams structure
Language:Rust1 0
digama0/theorem_proving_in_lean
Theorem proving in Lean
digama0/theorem_proving_in_lean4
Theorem Proving in Lean 4
Language:JavaScript
digama0/Unicode.lean
Unicode stuff for Lean 4! ✌️
Language:Lean