Issues

• Erdős Problem 297

  google-deepmind/formal-conjectures#7681 · Filter by author Nas01010101 opened on Oct 30, 2026

• W_3_21_eq (Green's Problem 14): w(2;3,21) = 416 is settled; Lean 4 proof deposited

  google-deepmind/formal-conjectures#7680 · Filter by author EitanNahmias opened on Oct 30, 2026

• WOWII 96: BFS-layer proof for nontrivial connected graphs (written proof for review)

  google-deepmind/formal-conjectures#7664 · Filter by author RhudeJJJJ opened on Oct 28, 2026
  1

• WOWII 84: induced-tree bound for graphs with a cut vertex (written proof for review)

  google-deepmind/formal-conjectures#7663 · Filter by author RhudeJJJJ opened on Oct 28, 2026

• WOWII 72: explicit counterexample and unbounded deficit (written proof for review)

  google-deepmind/formal-conjectures#7662 · Filter by author RhudeJJJJ opened on Oct 28, 2026

• OEIS A108569: the conjecture that all terms except the first are even is false (odd term 5095354107)

  google-deepmind/formal-conjectures#7643 · Filter by author Tetif opened on Oct 27, 2026

• Erdős 3: the linked ReciprocalProgressionTheorem is equivalent to erdos_3 as written — a kernel-checked bridge against the FC constant

  google-deepmind/formal-conjectures#7642 · Filter by author massimiliano1991 opened on Oct 27, 2026
  1

• CI: "Set up Python" fails on Ubuntu 26.04 runners

  google-deepmind/formal-conjectures#7628 · Filter by author veljjanoski opened on Oct 26, 2026

• Jeśmanowicz' conjecture on primitive Pythagorean triples and a^x + b^y = c^z

  google-deepmind/formal-conjectures#7626 · Filter by author Qunsheng-Zhang opened on Oct 26, 2026
  1

• Open question: are all extreme points of the 2×2 marginal body of shift-invariant measures on {0,1}^(ℤ²) periodic?

  new conjecture
  google-deepmind/formal-conjectures#7613 · Filter by author JarekDuda opened on Oct 25, 2026

• Proposed contribution: graph bootstrap percolation conjectures and supporting API

  google-deepmind/formal-conjectures#7597 · Filter by author Raj-Parekh24 opened on Oct 25, 2026

• Value-question answers that ignore a quantified parameter: Erdos 142, 319, 321, 361, 409 (sigma), 503, 692 (parts.ii)

  google-deepmind/formal-conjectures#7590 · Filter by author KilianTheMagnificent opened on Oct 24, 2026

• arXiv:2501.03234 (ArithmeticSumS): verified reduction of all four open conjectures to bounds on a single quantity rest(k), plus exact row identities

  google-deepmind/formal-conjectures#7589 · Filter by author Stayfoool opened on Oct 24, 2026

• Record a formal proof for R(3,3) = 6 (ramsey_number_three_three)

  google-deepmind/formal-conjectures#7573 · Filter by author Stayfoool opened on Oct 24, 2026

• Erdős Problem 1177: status mismatch (repo=solved, erdosproblems.com=open)

  erdos-status-sync
  google-deepmind/formal-conjectures#7569 · Filter by author github-actions opened on Oct 23, 2026

• Erdős 1063: add solved lower-bound variants with Lean proof links

  google-deepmind/formal-conjectures#7551 · Filter by author Paulee314 opened on Oct 23, 2026

• Erdős Problem 978: status mismatch (repo=formally solved, erdosproblems.com=open)

  erdos-status-sync
  google-deepmind/formal-conjectures#7547 · Filter by author github-actions opened on Oct 22, 2026

• Erdős Problem 659: status mismatch (repo=solved, erdosproblems.com=formally solved)

  erdos-status-syncformalisation exists elsewhere
  google-deepmind/formal-conjectures#7546 · Filter by author github-actions opened on Oct 22, 2026

• Erdős Problem 405: status mismatch (repo=solved, erdosproblems.com=formally solved)

  erdos-status-syncformalisation exists elsewhere
  google-deepmind/formal-conjectures#7545 · Filter by author github-actions opened on Oct 22, 2026

• Erdős Problem 43: status mismatch (repo=solved, erdosproblems.com=formally solved)

  erdos-status-syncformalisation exists elsewhere
  google-deepmind/formal-conjectures#7544 · Filter by author github-actions opened on Oct 22, 2026

• Erdős Problem 1119: status mismatch (repo=formally solved, erdosproblems.com=solved)

  erdos-status-sync
  google-deepmind/formal-conjectures#7543 · Filter by author github-actions opened on Oct 22, 2026

• Erdős Problem 732: status mismatch (repo=open, erdosproblems.com=solved)

  erdos-status-sync
  google-deepmind/formal-conjectures#7542 · Filter by author github-actions opened on Oct 22, 2026

• Erdős Problem 504: status mismatch (repo=formally solved, erdosproblems.com=solved)

  erdos-status-sync
  google-deepmind/formal-conjectures#7541 · Filter by author github-actions opened on Oct 22, 2026

• Erdős Problem 348: status mismatch (repo=solved, erdosproblems.com=open)

  erdos-status-sync
  google-deepmind/formal-conjectures#7540 · Filter by author github-actions opened on Oct 22, 2026

• General tracking issue for optimization constants

  google-deepmind/formal-conjectures#7524 · Filter by author BoltonBailey opened on Oct 22, 2026
  4