Discover @digama0 Open Source projects

Mario Carneiro (@digama0)

digama0

Stars
721
Global Rank 41,732 (Top 2 %)
Followers 385
Registered over 13 years ago
Most used languages

Rust
41.4 %

Lean 31.0 %

Objective-C++ 6.9 %

Java
6.9 %

HTML
6.9 %

Scala
3.4 %

TeX
3.4 %

mm0

Metamath Zero specification language

lean-type-theory

LaTeX code for a paper on lean's type theory

mmj2

mmj2 GUI Proof Assistant for the Metamath project

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

lean-sys

Rust bindings for the Lean 4 proof assistant

frat

DRAT proof processor

olean-rs

parser/viewer for olean files (lean 3)

MCRedstoneSim

Baezon's Redstone Simulator

dae-parser

Rust crate for parsing Collada DAE files

lean-rs

High level Lean 4 FFI for Rust

mm-hammer

A tool for automatically proving Metamath theorems using ATPs

advent-of-code

The Advent of Code programming puzzles in Lean

mm-web-rs

A metamath web site generator in rust

vc0

C0 specification and verified compiler in Lean

dtt.mm

Metamath database for dependent type theory

leangz

Lean 4 .olean file (de)compressor

mm-scala

A Metamath verifier in Scala

lean-cache

Lean 4 build cache management tool

lafny

Some experiments in Dafny-like syntax in Lean 4

oleandump

A type-aware olean tparser for Lean 4 olean files

coq-rs

A Coq .vo parser in Rust

ast_export

AST export from Lean 4

mathlib-ITP2019

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

minidom-14

kremlin

Lean port of the CompCert project in Coq, for the KreMLin compiler

digama0.github.io

My personal website

set.mm

Development of the set.mm mathematical database for the Metamath project