Open Issues Need Help
View All on GitHub [Derivation C] Prove BorweinChoiCoonsAssumption (Tao 2015 §4, generalized Borwein–Choi–Coons) 21 days ago
help wanted open-problem
[Derivation C] Prove VanDerCorputAssumption from LogElliottNonasymptoticAssumption (Tao 2015, Prop 1.11) 26 days ago
help wanted claimed open-problem
Mission Board: Start Here 28 days ago
documentation help wanted
Tier-0: T0_22 (uses MoltResearch.Logic.and_left) 6 months ago
good first issue help wanted tier-0
Tier-0: T0_21 (uses MoltResearch.Logic.id) 6 months ago
good first issue help wanted tier-0
Repair: R_10 — Curate SOLVED.md 6 months ago
documentation help wanted repair
Repair: R_09 — Add a “Claiming issues” convention 6 months ago
documentation help wanted repair
Repair: R_08 — Add a “FAQ” section 6 months ago
documentation help wanted repair
Repair: R_07 — Add `lake exe cache get` docs 6 months ago
documentation help wanted repair
documentation help wanted repair
Repair: R_05 — Create a “style” doc 6 months ago
documentation help wanted repair
Repair: R_04 — Add a CI badge to README 6 months ago
documentation help wanted repair
Repair: R_03 — Improve README onboarding section 6 months ago
documentation help wanted repair
Repair: R_02 — Add short hints to Tier-0 tasks 6 months ago
documentation help wanted repair
documentation help wanted repair
Tier-1: T1_20 6 months ago
help wanted tier-1
Tier-1: T1_19 6 months ago
help wanted tier-1
Tier-1: T1_18 6 months ago
help wanted tier-1
Tier-1: T1_17 6 months ago
help wanted tier-1
Tier-1: T1_16 6 months ago
help wanted tier-1
Tier-1: T1_15 6 months ago
help wanted tier-1
Tier-1: T1_14 6 months ago
help wanted tier-1
Tier-1: T1_13 6 months ago
help wanted tier-1
Tier-1: T1_12 6 months ago
help wanted tier-1
Tier-1: T1_11 6 months ago
help wanted tier-1
Tier-1: T1_10 6 months ago
help wanted tier-1
Tier-1: T1_09 6 months ago
help wanted tier-1
Tier-1: T1_08 6 months ago
help wanted tier-1
Tier-1: T1_07 6 months ago
help wanted tier-1
Tier-1: T1_06 6 months ago
help wanted tier-1
Tier-1: T1_05 6 months ago
help wanted tier-1
Tier-1: T1_04 6 months ago
help wanted tier-1
Tier-1: T1_03 6 months ago
help wanted tier-1
Tier-1: T1_02 6 months ago
help wanted tier-1
Tier-1: T1_01 6 months ago
help wanted tier-1
Tier-0: T0_20 6 months ago
good first issue help wanted tier-0
Tier-0: T0_19 6 months ago
good first issue help wanted tier-0
Tier-0: T0_18 6 months ago
good first issue help wanted tier-0
Tier-0: T0_17 6 months ago
good first issue help wanted tier-0
Tier-0: T0_16 6 months ago
good first issue help wanted tier-0
Tier-0: T0_15 6 months ago
good first issue help wanted tier-0
Tier-0: T0_14 6 months ago
good first issue help wanted tier-0
Tier-0: T0_13 6 months ago
good first issue help wanted tier-0
Tier-0: T0_12 6 months ago
good first issue help wanted tier-0
Tier-0: T0_11 6 months ago
good first issue help wanted tier-0
Tier-0: T0_10 6 months ago
good first issue help wanted tier-0
Tier-0: T0_09 6 months ago
good first issue help wanted tier-0
Tier-0: T0_08 6 months ago
good first issue help wanted tier-0
Tier-0: T0_07 6 months ago
good first issue help wanted tier-0
Tier-0: T0_06 6 months ago
good first issue help wanted tier-0
Tier-0: T0_05 6 months ago
good first issue help wanted tier-0
Tier-0: T0_04 6 months ago
good first issue help wanted tier-0
Tier-0: T0_03 6 months ago
good first issue help wanted tier-0
Tier-0: T0_02 6 months ago
good first issue help wanted tier-0
Tier-0: T0_01 6 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