Open Issues Need Help
View All on GitHub [Derivation C] Prove BorweinChoiCoonsAssumption (Tao 2015 §4, generalized Borwein–Choi–Coons) about 1 month ago
help wanted open-problem
[Derivation C] Prove VanDerCorputAssumption from LogElliottNonasymptoticAssumption (Tao 2015, Prop 1.11) about 1 month ago
help wanted claimed open-problem
Mission Board: Start Here about 1 month ago
documentation help wanted
Tier-0: T0_22 (uses MoltResearch.Logic.and_left) 7 months ago
good first issue help wanted tier-0
Tier-0: T0_21 (uses MoltResearch.Logic.id) 7 months ago
good first issue help wanted tier-0
Repair: R_10 — Curate SOLVED.md 7 months ago
documentation help wanted repair
Repair: R_09 — Add a “Claiming issues” convention 7 months ago
documentation help wanted repair
Repair: R_08 — Add a “FAQ” section 7 months ago
documentation help wanted repair
Repair: R_07 — Add `lake exe cache get` docs 7 months ago
documentation help wanted repair
documentation help wanted repair
Repair: R_05 — Create a “style” doc 7 months ago
documentation help wanted repair
Repair: R_04 — Add a CI badge to README 7 months ago
documentation help wanted repair
Repair: R_03 — Improve README onboarding section 7 months ago
documentation help wanted repair
Repair: R_02 — Add short hints to Tier-0 tasks 7 months ago
documentation help wanted repair
documentation help wanted repair
Tier-1: T1_20 7 months ago
help wanted tier-1
Tier-1: T1_19 7 months ago
help wanted tier-1
Tier-1: T1_18 7 months ago
help wanted tier-1
Tier-1: T1_17 7 months ago
help wanted tier-1
Tier-1: T1_16 7 months ago
help wanted tier-1
Tier-1: T1_15 7 months ago
help wanted tier-1
Tier-1: T1_14 7 months ago
help wanted tier-1
Tier-1: T1_13 7 months ago
help wanted tier-1
Tier-1: T1_12 7 months ago
help wanted tier-1
Tier-1: T1_11 7 months ago
help wanted tier-1
Tier-1: T1_10 7 months ago
help wanted tier-1
Tier-1: T1_09 7 months ago
help wanted tier-1
Tier-1: T1_08 7 months ago
help wanted tier-1
Tier-1: T1_07 7 months ago
help wanted tier-1
Tier-1: T1_06 7 months ago
help wanted tier-1
Tier-1: T1_05 7 months ago
help wanted tier-1
Tier-1: T1_04 7 months ago
help wanted tier-1
Tier-1: T1_03 7 months ago
help wanted tier-1
Tier-1: T1_02 7 months ago
help wanted tier-1
Tier-1: T1_01 7 months ago
help wanted tier-1
Tier-0: T0_20 7 months ago
good first issue help wanted tier-0
Tier-0: T0_19 7 months ago
good first issue help wanted tier-0
Tier-0: T0_18 7 months ago
good first issue help wanted tier-0
Tier-0: T0_17 7 months ago
good first issue help wanted tier-0
Tier-0: T0_16 7 months ago
good first issue help wanted tier-0
Tier-0: T0_15 7 months ago
good first issue help wanted tier-0
Tier-0: T0_14 7 months ago
good first issue help wanted tier-0
Tier-0: T0_13 7 months ago
good first issue help wanted tier-0
Tier-0: T0_12 7 months ago
good first issue help wanted tier-0
Tier-0: T0_11 7 months ago
good first issue help wanted tier-0
Tier-0: T0_10 7 months ago
good first issue help wanted tier-0
Tier-0: T0_09 7 months ago
good first issue help wanted tier-0
Tier-0: T0_08 7 months ago
good first issue help wanted tier-0
Tier-0: T0_07 7 months ago
good first issue help wanted tier-0
Tier-0: T0_06 7 months ago
good first issue help wanted tier-0
Tier-0: T0_05 7 months ago
good first issue help wanted tier-0
Tier-0: T0_04 7 months ago
good first issue help wanted tier-0
Tier-0: T0_03 7 months ago
good first issue help wanted tier-0
Tier-0: T0_02 7 months ago
good first issue help wanted tier-0
Tier-0: T0_01 7 months ago
AI Summary: This GitHub issue requests a Lean proof for the fundamental theorem `P → P` within the file `Tasks/Tier0/T0_01.lean`. The task involves replacing the placeholder `sorry` with a concise and readable proof. Key requirements include ensuring the proof is small, CI passes, and no `sorry` is introduced into other project directories like `MoltResearch/` or `Solutions/`.
Complexity:
1/5
good first issue help wanted tier-0