Pinned Repositories
arwm
Automated Reasoning for the Working Mathematician
boole
The Boole Interactive Reasoning Assistant
formal_methods_in_education
A web page with resources for teaching with formal methods and tools.
isabelle
working directory for Isabelle proof scripts
lamr
Logic and Mechanized Reasoning
logic_and_proof
CMU Undergrad Course
mathematics_in_lean
The user home repository for the Mathematics in Lean tutorial.
mathematics_in_lean_source
Source code for the Mathematics in Lean tutorial.
polya
A heuristic procedure for proving inequalities
qpf
Datatypes as quotients of polynomial functors
avigad's Repositories
avigad/lamr
Logic and Mechanized Reasoning
avigad/mathematics_in_lean_source
Source code for the Mathematics in Lean tutorial.
avigad/polya
A heuristic procedure for proving inequalities
avigad/qpf
Datatypes as quotients of polynomial functors
avigad/formal_methods_in_education
A web page with resources for teaching with formal methods and tools.
avigad/arwm
Automated Reasoning for the Working Mathematician
avigad/mathematics_in_lean
The user home repository for the Mathematics in Lean tutorial.
avigad/logic_and_proof
CMU Undergrad Course
avigad/verification_demo
A temporary repository
avigad/qelim
Quantifier elimination by computational reflection in Lean
avigad/formal_logic
A formalization of formal logic in Lean
avigad/mathlib
Lean mathematical components library
avigad/programming_in_lean
avigad/theorem_proving_in_lean
Theorem proving in Lean
avigad/theorem_proving_in_lean4
Theorem Proving in Lean 4
avigad/cairo
Cairo is the first Turing-complete language for creating provable programs for general computation.
avigad/cairo-lang
avigad/cvx
avigad/embed
avigad/group-representations
The definition and basic properties of representations of groups in the Lean theorem prover
avigad/lean-smt
Tactics for discharging Lean goals into SMT solvers.
avigad/leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.
avigad/leanprover.github.io
www
avigad/mathlib4
Work in progress mathlib port for lean 4
avigad/mathport
Mathport is a tool for porting Lean3 projects to Lean4
avigad/model-counting
Research on verified model counting
avigad/reference
Reference manual for the Lean theorem prover
avigad/smtlean
A Lean library of interfaces to SAT/SMT solvers (WIP)
avigad/verified-encodings
Verifying encodings into propositional logic in Lean
avigad/vscode-lean
An extension for VS Code which provides support for the Lean language.