Mario Carneiro

icon indicating a website link https://digama0.github.io/ icon indicating an email [email protected]

icon company Chalmers University of Technology icon location Gothenburg, Sweden icon location I'm a post-doc working on formal mathematics and interactive theorem proving. I am an expert in the Metamath and Lean proof languages.

Results 10 repositories owned by Mario Carneiro

advent-of-code

7
Stars
1
Forks
Watchers

The Advent of Code programming puzzles in Lean

verified publisher icon digama0

dtt.mm

5
Stars
0
Forks
Watchers

Metamath database for dependent type theory

verified publisher icon digama0

frat

15
Stars
2
Forks
Watchers

DRAT proof processor

verified publisher icon digama0

lean-type-theory

98
Stars
3
Forks
Watchers

LaTeX code for a paper on lean's type theory

verified publisher icon digama0

MCRedstoneSim

9
Stars
2
Forks
Watchers

Baezon's Redstone Simulator

verified publisher icon digama0

mm-lean4

16
Stars
1
Forks
Watchers

Lean 4 Metamath verifier

verified publisher icon digama0

mm0

276
Stars
40
Forks
Watchers

Metamath Zero specification language

verified publisher icon digama0

mmj2

71
Stars
24
Forks
Watchers

mmj2 GUI Proof Assistant for the Metamath project

verified publisher icon digama0

lean4lean

50
Stars
2
Forks
Watchers

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

verified publisher icon digama0

mizar-rs

39
Stars
4
Forks
Watchers

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

verified publisher icon digama0