Hacker GitHub

← All repos

google-deepmind/formal-conjectures

View on GitHub ↗ ★ 1,344 Lean

A collection of formalized statements of conjectures in Lean.

15 mentions on Hacker News by 10 people: 4 stories, 11 comments · first 2025-05-28 · latest 2026-10-09

Mentions per year 15 mentions · busiest year 2026 (8)
20082026
AllStoriesComments NewestTopOldest
  1. …of OpenAI's effort. No expert in PDEs or formal verification has disputed it as far as I'm aware. https://github.com/google-deepmind/formal-conjectures/blob/8...
    comment by fasterik · 2026-10-09 · in Navier–Stokes Lost in Translation
  2. …was proven in Lean. As of now at least, it's believed to be a correct statement of the problem. https://github.com/google-deepmind/formal-conjectures/blob/8...
    comment by fasterik · 2026-10-07 · in Navier–Stokes Lost in Translation
  3. …been accepted by the community as a valid formalization of the original Clay Institute statement. https://github.com/google-deepmind/formal-conjectures/blob/8...
    comment by fasterik · 2026-10-07 · in Navier–Stokes Lost in Translation
  4. They actually used Lean statements that were carefully human-written and human-reviewed, from here https://github.com/google-deepmind/formal-conjectures/blob/m... This doesn't guarantee that the statement is correct (Lean cannot do that),…
    comment by fpvandoorn · 2026-09-09 · in How An AI math breakthrough ignited a controversy
  5. Here's your Lean proof https://github.com/google-deepmind/formal-conjectures/pull/4...
    comment by rirze · 2026-07-20 · in Claude Fable produced a counterexample to the Jacobian Conjecture
  6. This has existed for a few months, but there aren't any reports of (unsuccessful) attempts: https://github.com/google-deepmind/formal-conjectures
    comment by 7373737373 · 2026-04-26 · in Amateur armed with ChatGPT solves an Erdős problem
  7. …as finding an error on some obscure line of a long proof. (There's also an older formulation at https://github.com/google-deepmind/formal-conjectures/blob/f... but the new one is more in the spirit of what was intended: see the discussion…
    comment by svat · 2026-01-10 · in “Erdos problem #728 was solved more or less autonomously by AI”
  8. Do you regularly test your AI on the https://github.com/google-deepmind/formal-conjectures collection?
    comment by 7373737373 · 2026-01-10 · in “Erdos problem #728 was solved more or less autonomously by AI”
  9. ▲ 2
    A collection of formalized statements of conjectures in Lean
    story by EvgeniyZh · 2025-09-08 · 0 comments
  10. …Polyhedron Rupert?" was added as a formal Lean statement to Google's Formal Conjectures repository: https://github.com/google-deepmind/formal-conjectures/blob/1... I wonder how feasible it would be to formalize this new proof in Lean.
    comment by dwrensha · 2025-08-29 · in Rupert's Property
  11. for reference, the statement has been formalized in Lean in Deepmind's open problem database: https://github.com/google-deepmind/formal-conjectures/blob/e...
    comment by 7373737373 · 2025-07-31 · in Slow
  12. They aren't - they are currently collating a repository of formalized open problems: https://github.com/google-deepmind/formal-conjectures
    comment by 7373737373 · 2025-07-21 · in Gemini with Deep Think achieves gold-medal standard at the IMO
  13. ▲ 1
    Google-DeepMind/formal-conjectures repository: formalized conjectures
    story by isaacfrond · 2025-06-17 · 0 comments
  14. ▲ 4
    Formal Conjectures
    story by md224 · 2025-05-30 · 0 comments
  15. ▲ 4
    Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean
    story by diginova · 2025-05-28 · 0 comments