Issues

• Lean proof of RH_up_to 14 and RH_up_to 15: which node should it go under? (depends on LeanCert, see #164)

  teorth/IEANTN#184 · Filter by author antoine-olivier opened on Oct 24, 2026

• Two docstrings state less than, or other than, their Lean declarations

  teorth/IEANTN#183 · Filter by author mlsimon734 opened on Oct 20, 2026

• Decide whether a verification run may depend on LeanCert

  teorth/IEANTN#164 · Filter by author teorth opened on Oct 17, 2026

• [DudekPlatt]: Recover exp(9658) under the repaired criterion, or show it cannot be

  teorth/IEANTN#63 · Filter by author teorth opened on Aug 30, 2026
  4

  

• [Buthe]: State the rest of the two Büthe papers — Table 1, Theorem 1, and a kind question

  teorth/IEANTN#56 · Filter by author teorth opened on Aug 29, 2026
  5

  

• [FKS]: Formalize the node — settle two discrepancies, then decide the split

  teorth/IEANTN#52 · Filter by author teorth opened on Aug 29, 2026
  10

  

• [BKLNW]: Formalize the node — split the pipeline from the numerics, and verify the pipeline

  teorth/IEANTN#50 · Filter by author teorth opened on Aug 29, 2026
  3