avigad Goto Github PK

arwm

Automated Reasoning for the Working Mathematician

auto

A tableau prover for Lean

boole

The Boole Interactive Reasoning Assistant

cairo

Cairo is the first Turing-complete language for creating provable programs for general computation.

cairo-lang

cmu-15815-s15

CMU 15-815 Spring 2015 : Interactive Theorem Proving

cvx

embed

formal_logic

A formalization of formal logic in Lean

formal_methods_in_education

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

group-representations

The definition and basic properties of representations of groups in the Lean theorem prover

hott3

HoTT in Lean 3

introduction_to_lean

isabelle

working directory for Isabelle proof scripts

lamr

Logic and Mechanized Reasoning

lean

Lean Theorem Prover

lean-smt

Tactics for discharging Lean goals into SMT solvers.

lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)

lean_reference

A temporary repository with a start on the Lean reference manual

leanproved

Theorems proved using the Lean prover.

leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.

leanprover.github.io

www

libraries

Lean Libraries

library_dev

Lean standard library (development)

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.

mathlib

Lean mathematical components library

mathlib4

Work in progress mathlib port for lean 4

mathport

Mathport is a tool for porting Lean3 projects to Lean4