Jeremy Avigad

mathematics_in_lean_source. Source code for the Mathematics in Lean tutorial.

lamr. Logic and Mechanized Reasoning

qpf. Datatypes as quotients of polynomial functors

polya. A heuristic procedure for proving inequalities

boole. The Boole Interactive Reasoning Assistant

formal_methods_in_education. A web page with resources for teaching with formal methods and tools.

arwm. Automated Reasoning for the Working Mathematician

LeanSudoku. Playing Sudoku in the Lean 4 proof assistant

logic_and_proof. CMU Undergrad Course

isabelle. working directory for Isabelle proof scripts

mathematics_in_lean. The user home repository for the Mathematics in Lean tutorial.

lafny-experiments. A repository for experimenting on methods of code verification in Lean

auto. A tableau prover for Lean

verification_demo. A temporary repository

qelim. Quantifier elimination by computational reflection in Lean

programming_in_lean. TeX

EquationalTest. A test of Duper with an example from the Equational Theories project

formal_logic. A formalization of formal logic in Lean

library_dev. Lean standard library (development)

cmu-15815-s15. CMU 15-815 Spring 2015 : Interactive Theorem Proving

theorem_proving_in_lean. Theorem proving in Lean

theorem_proving_in_lean4. Theorem Proving in Lean 4

mathlib. Lean mathematical components library