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:Rust12 2 01
lean-sys
Rust bindings for the Lean 4 proof assistant
Language:Rust19 2 26
lean-type-theory
LaTeX code for a paper on lean's type theory
Language:TeX121 6 14
lean4lean
Lean 4 kernel / 'external checker' written in Lean 4
Language:Lean74 6 16
mizar-rs
Alternative Mizar proof checker (http://mizar.org/) written in Rust
Language:Rust47 7 94
mm-lean4
Lean 4 Metamath verifier
Language:Lean16 5 01
mm0
Metamath Zero specification language
Language:Lean317 21 5840
mmj2
mmj2 GUI Proof Assistant for the Metamath project
Language:Java72 11 3926
mathlib3
Lean 3's obsolete mathematical components library: please use mathlib4
Language:Lean1.7k 53 362298

digama0's Repositories

digama0/mm0
Metamath Zero specification language
Language:Lean317 21 5840
digama0/lean4lean
Lean 4 kernel / 'external checker' written in Lean 4
Language:Lean74 6 16
digama0/mmj2
mmj2 GUI Proof Assistant for the Metamath project
Language:Java72 11 3926
digama0/mizar-rs
Alternative Mizar proof checker (http://mizar.org/) written in Rust
Language:Rust47 7 94
digama0/lean-sys
Rust bindings for the Lean 4 proof assistant
Language:Rust19 2 26
digama0/lean-rs
High level Lean 4 FFI for Rust
Language:Rust12 2 01
digama0/dae-parser
Rust crate for parsing Collada DAE files
Language:Rust9 3 20
digama0/mm-hammer
A tool for automatically proving Metamath theorems using ATPs
Language:Rust9 4 02
digama0/ast_export
AST export from Lean 4
Language:Lean7 1 0
digama0/leangz
Lean 4 .olean file (de)compressor
Language:Rust5 3 21
digama0/mm-web-rs
A metamath web site generator in rust
Language:HTML5 5 5
digama0/oleandump
A type-aware olean tparser for Lean 4 olean files
Language:Lean3 2 01
digama0/digama0.github.io
My personal website
Language:HTML1 2 0
digama0/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Language:TeX1 0 0
digama0/hol4-vscode
HOL4 mode for VSCode
1
digama0/lean4checker
Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
Language:Lean1 1 0
digama0/minidom-14
Language:Rust1 2 11
digama0/verbose-lean4
Natural language tactics to teach mathematics using Lean 4
Language:Lean1 1 0
digama0/bors-ng
👁 A merge bot for GitHub Pull Requests
Language:Elixir1 0
digama0/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Language:OCaml0 0
digama0/equational_theories
A project to map out the relations between different equational theories of Magmas.
digama0/HOL
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
digama0/isabelle
Fork of https://isabelle-dev.sketis.net so I can use git
Language:Isabelle1 0
digama0/isabelle-rs
Parser for isabelle database files
Language:Rust1 0
digama0/lean4
Lean 4 programming language and theorem prover
Language:Lean2 0
digama0/LeanColls
WIP collections library for Lean 4
Language:Lean1 0
digama0/LeanSAT
Language:Lean1 0
digama0/moonrider
🌕🏄🏿 Surf the musical road among the stars. Side project built by two people in a few months to demonstrate WebXR.
Language:JavaScript1 0
digama0/polyml
Poly/ML
digama0/vscode-lean4
Visual Studio Code extension for the Lean 4 proof assistant
Language:TypeScript1 0