Following up on the Lean Zulip thread where @chenson2018 noted that "the most interesting part is likely thinking about and setting up the exact statement of what you want to verify" — specifically pointing at the relationship between "optimal" N-TET and the continued fraction.
The claim file is now tightened against current mathlib4:
https://github.com/thefalsework/papers/blob/main/validation/claims/optimal-ntet-continued-fraction.md
Two theorem statements are given — (C1) best-approximation-of-the-second-kind for the convergents of α = log₂(3/2) and (C2) the equivalence between strict-best-so-far Pythagorean temperaments and convergent-denominator record-holders — bound to live mathlib primitives (Real.convergent, Irrational, Real.logb, round). The file also enumerates four specific statement-level questions a validator is invited to answer.
Ask: statement-level feedback on whether the shape is right to be provable, independent of whether the proofs exist. Both kinds of feedback are useful:
- Math-level — is (C1) or (C2) stated correctly? Is the record-holder framing in (C2) the right form, or is there a cleaner one?
- Carrier-level — the signatures are written against the mathlib API docs but have not been type-checked locally. If there are naming or coercion issues that would prevent
lake build, flagging those is useful too.
@chenson2018 — tagging you since your Zulip note prompted the tightening. No obligation and no hurry; equally happy if other Lean contributors want to engage. Discussion here or on the claim file is welcome.
Following up on the Lean Zulip thread where @chenson2018 noted that "the most interesting part is likely thinking about and setting up the exact statement of what you want to verify" — specifically pointing at the relationship between "optimal" N-TET and the continued fraction.
The claim file is now tightened against current mathlib4:
https://github.com/thefalsework/papers/blob/main/validation/claims/optimal-ntet-continued-fraction.md
Two theorem statements are given — (C1) best-approximation-of-the-second-kind for the convergents of
α = log₂(3/2)and (C2) the equivalence between strict-best-so-far Pythagorean temperaments and convergent-denominator record-holders — bound to live mathlib primitives (Real.convergent,Irrational,Real.logb,round). The file also enumerates four specific statement-level questions a validator is invited to answer.Ask: statement-level feedback on whether the shape is right to be provable, independent of whether the proofs exist. Both kinds of feedback are useful:
lake build, flagging those is useful too.@chenson2018 — tagging you since your Zulip note prompted the tightening. No obligation and no hurry; equally happy if other Lean contributors want to engage. Discussion here or on the claim file is welcome.