Owner

lean-catLogic

1 indexed repository · View on GitHub

formalization
Formalization of Categorical Logic in the Lean proof assistant

Lean · 5 stars

Beginner friendly Everything

Open All

Develop theory of syntactic posets (Lindenbaum-Tarski algebras) Open

category theory semantics

Difficulty 5/5 Over a week Newbie friendliness 25/100

lean-catLogic/formalization#13 · Opened Mar 15, 2023
Document how the LiftT and HeavyLiftT tactics work Open

documentation tactics

Difficulty 2/5 1-3 hours Newbie friendliness 45/100

lean-catLogic/formalization#12 · Opened Mar 15, 2023
More proof calculi (and corresponding semantic structures) Open

enhancement good first issue semantics syntax & proof theory

Difficulty 5/5 Over a week Newbie friendliness 25/100

lean-catLogic/formalization#10 · Opened Mar 15, 2023
Use mathlib's definition of finite product cat & CCC Open

category theory good first issue

Difficulty 5/5 Over a week Newbie friendliness 25/100

lean-catLogic/formalization#8 · Opened Mar 15, 2023
Improve synCat cleanup & thin_cat.by_thin tactics Open

tactics

Difficulty 5/5 Over a week Newbie friendliness 20/100

lean-catLogic/formalization#7 · 1 comment · Opened Mar 3, 2023
Proof that downset is a CCC is gross Open

category theory

Difficulty 4/5 3-5 days Newbie friendliness 35/100

lean-catLogic/formalization#3 · 1 comment · Opened Feb 24, 2023

A short digest of beginner-friendly GitHub issues.