- key: ErdosProblems.Erdos2
  epc: https://www.erdosproblems.com/2
  author:
    informal:
      human:
        - Paul Balister
        - Béla Bollobás
        - Robert Morris
        - Julian Sahasrabudhe
        - Marius Tiba
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  arxiv: https://arxiv.org/abs/1811.03547
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos2.md
  version: "4.33.0"

- key: ErdosProblems.Erdos6
  epc: https://www.erdosproblems.com/6
  author:
    informal:
      human:
        - William D. Banks
        - Tristan Freiberg
        - Caroline L. Turnage-Butterbaugh
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  arxiv: https://arxiv.org/abs/1311.7003
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos6.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/6.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos8
  epc: https://www.erdosproblems.com/8
  author:
    informal:
      human:
        - Bob Hough
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos8.md
  version: "4.33.0"

- key: ErdosProblems.Erdos13
  epc: https://www.erdosproblems.com/13
  author:
    informal:
      human:
        - Borys Bedert
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos13.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/13.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos16
  epc: https://www.erdosproblems.com/16
  author:
    informal:
      human: Yong-Gao Chen
    formal:
      AI:
        - Gemini 3.1 Pro
        - Antigravity
      human: Daniel Chin
  arxiv: https://arxiv.org/abs/2312.04120
  url:
    - https://github.com/danielchin/proofs/blob/main/Proofs/ErdosProblems/Erdos16.lean
    - https://www.erdosproblems.com/forum/thread/16#post-4464
  version: "4.24.0"

- key: ErdosProblems.Erdos21
  epc: https://www.erdosproblems.com/21
  author:
    informal:
      human:
        - Jeff Kahn
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos21.md
  version: "4.33.0"

- key: ErdosProblems.Erdos22
  epc: https://www.erdosproblems.com/22
  author:
    informal:
      human:
        - Jacob Fox
        - Po-Shen Loh
        - Yufei Zhao
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos22.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/22.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos24
  epc: https://www.erdosproblems.com/24
  author:
    informal:
      human: Andrzej Grzesik
    formal:
      AI: Aristotle
      human: Matteo Del Vecchio
  arxiv: https://arxiv.org/abs/1102.0962
  url:
    - https://www.erdosproblems.com/forum/thread/24#post-5732
    - https://gist.githubusercontent.com/madeve-unipi/683739094ab7a5079a2bc2647c47743b/raw/6164255a2f1ed85df3f01b75d2f8b35a1330aacb/Erdos24.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos26
  epc: https://www.erdosproblems.com/26
  author:
    informal:
      human: Imre Ruzsa
    statement:
      - Formal Conjectures authors
      - Salvatore Mercuri
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/26
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos26.md
  version: "4.24.0"
  todo:
    - Google DeepMind's proof
    - Wouter van Doorn's comment

- key: ErdosProblems.Erdos27
  epc: https://www.erdosproblems.com/27
  author:
    informal:
      human:
        - Michael Filaseta
        - Kevin Ford
        - Sergei Konyagin
        - Carl Pomerance
        - Gang Yu
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos27.md
  version: "4.33.0"

- key: ErdosProblems.Erdos29
  epc: https://www.erdosproblems.com/29
  author:
    informal:
      human:
        - Paul Erdős
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos29.md
  version: "4.33.0"

- key: ErdosProblems.Erdos31
  epc: https://www.erdosproblems.com/31
  author:
    informal:
      human:
        - G. G. Lorentz
        - Wouter van Doorn
      AI: ChatGPT 5.1 Pro
    statement:
      human:
        - Formal Conjectures authors
        - Boris Alexeev
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/31
    - https://www.erdosproblems.com/forum/thread/31#post-1779
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos31.md
  version:
    - "4.20.0-rc5"
    - "4.24.0"

- key: ErdosProblems.Erdos34
  epc: https://www.erdosproblems.com/34
  author:
    informal:
      human:
        - N. Hegyvári
        - J. Konieczny
    formal:
      AI: Aristotle
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/1504.07156
  url:
    - https://www.erdosproblems.com/forum/thread/34
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos34.md
  version: "4.24.0"

- key: ErdosProblems.Erdos35
  epc: https://www.erdosproblems.com/35
  author:
    informal:
      human:
        - Helmut Plünnecke
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos35.md
  version: "4.33.0"

- key: ErdosProblems.Erdos37
  epc: https://www.erdosproblems.com/37
  author:
    informal:
      human:
        - Imre Ruzsa
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos37.md
  version: "4.33.0"

- key: ErdosProblems.Erdos38
  epc: https://www.erdosproblems.com/38
  author:
    informal:
      AI: GPT-5.5 Pro
      human: gebyjaff
    formal:
      AI: Aristotle
      human: Matteo Del Vecchio
  url:
    - https://www.erdosproblems.com/forum/thread/38#post-6131
    - https://gist.githubusercontent.com/madeve-unipi/690d2bd8f6e8304ba8b456f9db559747/raw/481e3c35de8dce7af70ec440e4e121f084a61860/Erdos38.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos42
  epc: https://www.erdosproblems.com/42
  author:
    informal:
      AI: GPT-5.5 Pro
      human: Harjas Sandhu
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex 5.5
        - GPT-5.5 Pro
      human: Pawan Sasanka Ammanamanchi
  url:
    - https://www.erdosproblems.com/forum/thread/42#post-6370
    - https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P42/CompactCayley/Proof.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/42.lean
    - https://raw.githubusercontent.com/Shashi456/erdos-formalizations/refs/heads/main/Erdos/P42/CompactCayley/Proof.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos43
  epc: https://www.erdosproblems.com/43
  author:
    informal:
      human:
        - Kevin Barreto
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos43.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/43.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos45
  epc: https://www.erdosproblems.com/45
  author:
    informal:
      human: Ernest S. Croot III
    formal:
      human:
        - Bhavik Mehta
        - Thomas Bloom
  arxiv: https://arxiv.org/abs/math/0311421
  url: https://github.com/b-mehta/unit-fractions
  version: "3.42.1"

- key: ErdosProblems.Erdos46
  epc: https://www.erdosproblems.com/46
  author:
    informal:
      human: Ernest S. Croot III
    formal:
      human:
        - Bhavik Mehta
        - Thomas Bloom
  arxiv: https://arxiv.org/abs/math/0311421
  url: https://github.com/b-mehta/unit-fractions
  version: "3.42.1"

- key: ErdosProblems.Erdos47
  epc: https://www.erdosproblems.com/47
  author:
    informal:
      human: Thomas Bloom
    formal:
      human:
        - Bhavik Mehta
        - Thomas Bloom
  arxiv: https://arxiv.org/abs/2112.03726
  url: https://github.com/b-mehta/unit-fractions
  version: "3.42.1"

- key: ErdosProblems.Erdos48
  epc: https://www.erdosproblems.com/48
  author:
    informal:
      human:
        - Kevin Ford
        - Florian Luca
        - Carl Pomerance
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos48.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/48.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos49
  epc: https://www.erdosproblems.com/49
  author:
    informal:
      human:
        - Terence Tao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos49.md
  version: "4.33.0"

- key: ErdosProblems.Erdos53
  epc: https://www.erdosproblems.com/53
  author:
    informal:
      human:
        - Paul Erdős
        - Endre Szemerédi
        - Mei-Chu Chang
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos53.md
  version: "4.33.0"

- key: ErdosProblems.Erdos54
  epc: https://www.erdosproblems.com/54
  author:
    informal:
      human:
        - David Conlon
        - Jacob Fox
        - Huy Tuan Pham
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos54.md
  version: "4.33.0"

- key: ErdosProblems.Erdos55
  epc: https://www.erdosproblems.com/55
  author:
    informal:
      human:
        - David Conlon
        - Jacob Fox
        - Huy Tuan Pham
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos55.md
  version: "4.33.0"

- key: ErdosProblems.Erdos56
  epc: https://www.erdosproblems.com/56
  author:
    informal:
      human:
        - Rudolf Ahlswede
        - Levon H. Khachatrian
      AI: ChatGPT
    statement:
      human:
        - Formal Conjectures authors
        - Boris Alexeev
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/56
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos56.md
  version:
    - "4.20.0-rc5"
    - "4.24.0"

- key: ErdosProblems.Erdos57
  epc: https://www.erdosproblems.com/57
  author:
    informal:
      human:
        - Paul Erdős
        - András Hajnal
        - Hong Liu
        - Richard Montgomery
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos57.md
  version: "4.33.0"

- key: ErdosProblems.Erdos58
  epc: https://www.erdosproblems.com/58
  author:
    informal:
      human:
        - András Gyárfás
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos58.md
  version: "4.33.0"

- key: ErdosProblems.Erdos59
  epc: https://www.erdosproblems.com/59
  author:
    informal:
      human:
        - Paul Erdős
        - Péter Frankl
        - Vojtěch Rödl
        - Robert Morris
        - David Saxton
        - Zoltán Füredi
        - Assaf Naor
        - Jacques Verstraëte
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos59.md
  version: "4.33.0"

- key: ErdosProblems.Erdos63
  epc: https://www.erdosproblems.com/63
  author:
    informal:
      human:
        - Hong Liu
        - Richard Montgomery
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos63.md
  version: "4.33.0"

- key: ErdosProblems.Erdos71
  epc: https://www.erdosproblems.com/71
  author:
    informal:
      human: Béla Bollobás
    formal:
      AI:
        - Aristotle
        - GPT-5.5
        - Opus 4.7
      human: Andres Gutierrez
  url:
    - https://www.erdosproblems.com/forum/thread/71#post-6635
  url_ref: andresg535_71
  version: "4.28.0"

- key: ErdosProblems.Erdos72
  epc: https://www.erdosproblems.com/72
  author:
    informal:
      human:
        - Jacques Verstraëte
        - Hong Liu
        - Richard Montgomery
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos72.md
  version: "4.33.0"

- key: ErdosProblems.Erdos79
  epc: https://www.erdosproblems.com/79
  author:
    informal:
      human:
        - Yufei Wigderson
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos79.md
  version: "4.33.0"

- key: ErdosProblems.Erdos83
  epc: https://www.erdosproblems.com/83
  author:
    informal:
      human:
        - Rudolf Ahlswede
        - Levon H. Khachatrian
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos83.md
  version: "4.33.0"

- key: ErdosProblems.Erdos88
  epc: https://www.erdosproblems.com/88
  author:
    informal:
      human:
        - Matthew Kwan
        - Ashwin Sah
        - Lisa Sauermann
        - Mehtaab Sawhney
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos88.md
  version: "4.33.0"

- key: ErdosProblems.Erdos92
  epc: https://www.erdosproblems.com/92
  author:
    informal:
      human:
        - L. Alpöge
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos92.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/92.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos93
  epc: https://www.erdosproblems.com/93
  author:
    informal:
      human: E. Altman
    formal:
      AI:
        - Gemini 3.0 Flash/Pro
        - Claude Opus 4.5/4.6
        - Numina Lean Agent
        - Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/93#post-4346
  url_ref: JoshuaB_93
  version: "4.24.0"

- key: ErdosProblems.Erdos94
  epc: https://www.erdosproblems.com/94
  author:
    informal:
      human:
        - Peter C. Fishburn
        - Hanno Lefmann
        - Torsten Thiele
      AI: ChatGPT 5.2 Thinking
    formal:
      AI:
        - ChatGPT 5.2 Thinking
        - Codex
      human: Li Ding
  url:
    - https://www.erdosproblems.com/forum/thread/94#post-3208
    - https://github.com/SpringSense-Innovation-Institute/ai-for-math-lean/blob/main/erdos-problems/erdos94/erdos94.lean
  version: "4.21.0"
  todo: Add Erdos94b with the SeedProver proof.

- key: ErdosProblems.Erdos95
  epc: https://www.erdosproblems.com/95
  author:
    informal:
      human:
        - Larry Guth
        - Nets Hawk Katz
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos95.md
  version: "4.33.0"

- key: ErdosProblems.Erdos105
  epc: https://www.erdosproblems.com/105
  author:
    informal:
      human: Wu Xichuan
    formal:
      AI:
        - ChatGPT Pro (Thinking)
        - Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/105#post-1430
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos105.md
  version:
    - "4.20.0-rc5"
    - "4.24.0"

- key: ErdosProblems.Erdos106
  epc: https://www.erdosproblems.com/106
  author:
    informal:
      human:
        - A. Raj Singh
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos106.md
  version: "4.33.0"

- key: ErdosProblems.Erdos109
  epc: https://www.erdosproblems.com/109
  author:
    informal:
      human:
        - Joel Moreira
        - Florian K. Richter
        - Donald Robertson
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos109.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/109.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos110
  epc: https://www.erdosproblems.com/110
  author:
    informal:
      human:
        - Chris Lambie-Hanson
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos110.md
  version: "4.33.0"

- key: ErdosProblems.Erdos113
  epc: https://www.erdosproblems.com/113
  author:
    informal:
      human:
        - Oliver Janzer
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos113.md
  version: "4.33.0"

- key: ErdosProblems.Erdos115
  epc: https://www.erdosproblems.com/115
  author:
    informal:
      human:
        - Alexandre Eremenko
        - Laszlo Lempert
    formal:
      AI:
        - Gemini 3.0 Flash
        - Gemini 3.1 Pro
        - Claude Sonnet 4.6
        - Claude Opus 4.6
        - Aristotle
        - ulam.ai scaffold
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/115#post-4555
  url_ref: JoshuaB_115
  version: "4.24.0"

- key: ErdosProblems.Erdos116
  epc: https://www.erdosproblems.com/116
  author:
    informal:
      human:
        - Christian Pommerenke
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos116.md
  version: "4.33.0"

- key: ErdosProblems.Erdos119
  epc: https://www.erdosproblems.com/119
  author:
    informal:
      AI: ChatGPT 5.6 Pro
      human: Samuel Korsky
    statement: Formal Conjectures authors
    formal:
      AI: Codex
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/119/proof-claims#proof-claim-7
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/119.lean
  version: "4.32.0"

- key: ErdosProblems.Erdos121
  epc: https://www.erdosproblems.com/121
  author:
    informal:
      human:
        - Terence Tao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos121.md
  version: "4.33.0"

- key: ErdosProblems.Erdos123
  epc: https://www.erdosproblems.com/123
  author:
    - Star Fleet Math
    - AI: Claude Fable 5
    - human: Colin Snyder
    - statement: Formal Conjectures authors
  url:
    - https://www.starfleetmath.com/
    - https://www.erdosproblems.com/forum/thread/123/proof-claims
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/123.lean
    - https://www.starfleetmath.com/downloads/verify/erdos-123/erdos-123-solution.zip
  version: "4.31.0"

- key: ErdosProblems.Erdos124b
  partial: yes
  epc: https://www.erdosproblems.com/124
  author:
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/124
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos124b.md
  version: "4.24.0"

- key: ErdosProblems.Erdos125
  epc: https://www.erdosproblems.com/125
  author:
    informal:
      AI: a DeepMind prover agent
    formal:
      AI: a DeepMind prover agent
      human: George Tsoukalas
  url:
    - https://www.erdosproblems.com/forum/thread/125#post-4448
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/125.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/300bf771bdbef43d7b9aa2521e633a50fd54dd28/FormalConjectures/ErdosProblems/125.lean
  version: "4.22.0"
  todo: Import this proof.

- key: ErdosProblems.Erdos127
  epc: https://www.erdosproblems.com/127
  author:
    informal:
      human:
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos127.md
  version: "4.33.0"

- key: ErdosProblems.Erdos133
  epc: https://www.erdosproblems.com/133
  author:
    informal:
      human:
        - David Hanson
        - Kathy Seyffarth
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos133.md
  version: "4.33.0"

- key: ErdosProblems.Erdos134
  epc: https://www.erdosproblems.com/134
  author:
    informal:
      human: Noga Alon
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/134
    - https://web.math.princeton.edu/~nalon/PDFS/remark1901.pdf
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos134.md
  version: "4.24.0"

- key: ErdosProblems.Erdos135
  epc: https://www.erdosproblems.com/135
  author:
    informal:
      human:
        - Terence Tao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos135.md
  version: "4.33.0"

- key: ErdosProblems.Erdos136
  epc: https://www.erdosproblems.com/136
  author:
    informal:
      human:
        - Patrick Bennett
        - Ryan Cushman
        - Andrzej Dudek
        - Paweł Prałat
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos136.md
  version: "4.33.0"

- key: ErdosProblems.Erdos139
  epc: https://www.erdosproblems.com/139
  author:
    informal:
      human:
        - Endre Szemerédi
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos139.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/139.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos140
  epc: https://www.erdosproblems.com/140
  author:
    informal:
      human:
        - Zachary Kelley
        - Raghu Meka
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos140.md
  version: "4.33.0"

- key: ErdosProblems.Erdos144
  epc: https://www.erdosproblems.com/144
  author:
    informal:
      human:
        - Helmut Maier
        - Gérald Tenenbaum
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos144.md
  version: "4.33.0"

- key: ErdosProblems.Erdos146
  epc: https://www.erdosproblems.com/146
  author:
    informal:
      AI: Astra (internal OpenAI model)
    formal:
      AI: Astra (internal OpenAI model)
      human: OpenAI team
  url:
    - https://www.erdosproblems.com/forum/thread/146#post-8253
    - https://github.com/openai/ten-proofs/blob/a13547c6be4563746881d0b3b4c9fd03f72f0484/CompactnessAndDegeneracy.lean
    - https://openai.com/index/ten-advances-in-mathematics/
  version: "4.32.0"

- key: ErdosProblems.Erdos147
  epc: https://www.erdosproblems.com/147
  author:
    informal:
      human:
        - Oliver Janzer
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos147.md
  version: "4.33.0"

- key: ErdosProblems.Erdos150
  epc: https://www.erdosproblems.com/150
  author:
    informal:
      human: Domagoj Bradač
    formal:
      AI: Aristotle
      human: Pietro Monticone
  arxiv: https://arxiv.org/abs/2409.02974
  url:
    - https://www.erdosproblems.com/forum/thread/150#post-5145
    - https://gist.githubusercontent.com/pitmonticone/d8558d3361ad2d673b5405239ea30700/raw/c966009555b83985762dac9faaf705aad3f48199/Erdos150.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos152
  epc: https://www.erdosproblems.com/152
  author:
    informal:
      human:
        - Paul Erdős
        - András Sárközy
        - Vera T. Sós
      AI:
        - DeepMind prover agent
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos152.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/152.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos154
  epc: https://www.erdosproblems.com/154
  author:
    informal:
      human: Bernt Lindström
      AI: ChatGPT
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/154#post-4218
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem154.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos163
  epc: https://www.erdosproblems.com/163
  author:
    informal:
      human:
        - Choongbum Lee
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos163.md
  version: "4.33.0"

- key: ErdosProblems.Erdos164
  epc: https://www.erdosproblems.com/164
  author:
    formal:
      AI: Codex
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/164
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos164.md
  version: "4.29.0"

- key: ErdosProblems.Erdos166
  epc: https://www.erdosproblems.com/166
  author:
    informal:
      human:
        - Sam Mattheus
        - Jacques Verstraëte
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos166.md
  version: "4.33.0"

- key: ErdosProblems.Erdos171
  epc: https://www.erdosproblems.com/171
  author:
    informal:
      human:
        - Pandelis Dodos
        - Vassilis Kanellopoulos
        - Konstantinos Tyros
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos171.md
  version: "4.33.0"

- key: ErdosProblems.Erdos175
  epc: https://www.erdosproblems.com/175
  author:
    informal:
      human:
        - Andrew Granville
        - Olivier Ramaré
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos175.md
  version: "4.33.0"

- key: ErdosProblems.Erdos178
  epc: https://www.erdosproblems.com/178
  author:
    informal:
      human: József Beck
    formal:
      AI: Aristotle
      human: Matteo Del Vecchio
  url:
    - https://www.erdosproblems.com/forum/thread/178#post-5685
    - https://gist.githubusercontent.com/madeve-unipi/ca9c3d1f94fe124c15726d836e1cd623/raw/a272de656847d3956e1c228c833ff3c591dc4872/Erdos178.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos179
  epc: https://www.erdosproblems.com/179
  author:
    informal:
      human:
        - Jacob Fox
        - Cosmin Pohoata
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos179.md
  version: "4.33.0"

- key: ErdosProblems.Erdos180
  epc: https://www.erdosproblems.com/180
  author:
    informal:
      AI: Astra (internal OpenAI model)
    formal:
      AI: Astra (internal OpenAI model)
      human: OpenAI team
  url:
    - https://www.erdosproblems.com/forum/thread/180#post-8255
    - https://github.com/openai/ten-proofs/blob/a13547c6be4563746881d0b3b4c9fd03f72f0484/CompactnessAndDegeneracy.lean
    - https://openai.com/index/ten-advances-in-mathematics/
  version: "4.32.0"

- key: ErdosProblems.Erdos182
  epc: https://www.erdosproblems.com/182
  author:
    informal:
      human:
        - Oliver Janzer
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos182.md
  version: "4.33.0"

- key: ErdosProblems.Erdos183
  epc: https://www.erdosproblems.com/183
  author:
    informal:
      AI: Astra (internal OpenAI model)
    formal:
      AI: Astra (internal OpenAI model)
      human: OpenAI team
  url:
    - https://www.erdosproblems.com/forum/thread/183#post-8250
    - https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6/MulticolorTriangleRamsey.lean
    - https://openai.com/index/ten-advances-in-mathematics/
  version: "4.32.0"

- key: ErdosProblems.Erdos185
  epc: https://www.erdosproblems.com/185
  author:
    informal:
      human:
        - Pandelis Dodos
        - Vassilis Kanellopoulos
        - Konstantinos Tyros
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos185.md
  version: "4.33.0"

- key: ErdosProblems.Erdos186
  epc: https://www.erdosproblems.com/186
  author:
    informal:
      human:
        - Károly Bosznay
        - Huy Tuan Pham
        - Dmitrii Zakharov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos186.md
  version: "4.33.0"

- key: ErdosProblems.Erdos189
  epc: https://www.erdosproblems.com/189
  author:
    informal:
      human: Vjekoslav Kovač
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Vjekoslav Kovač
  arxiv: https://arxiv.org/abs/2309.09973
  url:
    - https://www.erdosproblems.com/forum/thread/189
    - https://web.math.pmf.unizg.hr/~vjekovac/EP/EP189/Erdos189_blueprint.tex
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos189.md
  version: "4.24.0"

- key: ErdosProblems.Erdos190
  epc: https://www.erdosproblems.com/190
  author:
    informal:
      human:
        - J. H. Bae
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos190.md
  version: "4.33.0"

- key: ErdosProblems.Erdos191
  epc: https://www.erdosproblems.com/191
  author:
    informal:
      human:
        - Vojtěch Rödl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos191.md
  version: "4.33.0"

- key: ErdosProblems.Erdos194
  epc: https://www.erdosproblems.com/194
  author:
    informal:
      human:
        - Hayri Ardal
        - Tom Brown
        - Veselin Jungić
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Stefano Rocca
  url:
    - https://www.erdosproblems.com/forum/thread/194#post-5430
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/194.lean
    - https://gist.githubusercontent.com/ster-oc/ffe9e4fa1b813111f40c0e417bbe8be0/raw/6f748a76e55d47e24ca319a9c00fd20ab79422bb/Erdos194.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos198
  epc: https://www.erdosproblems.com/198
  author:
    informal:
      human: James E. Baumgartner
      AI:
        - ChatGPT 5.1 Pro
        - AlphaProof
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/198
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos198.md
  version:
    - "4.20.0-rc5"
    - "4.24.0"

- key: ErdosProblems.Erdos199
  epc: https://www.erdosproblems.com/199
  author:
    informal:
      human: James E. Baumgartner
    formal:
      AI: Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/199#post-4442
  url_ref: JoshuaB_199
  version: "4.24.0"

- key: ErdosProblems.Erdos202
  epc: https://www.erdosproblems.com/202
  author:
    informal:
      AI: GPT-5.4 Pro
      human: Boon Suan Ho
    formal:
      AI: Claude
      human: Pawan Sasanka Ammanamanchi
  url:
    - https://www.erdosproblems.com/forum/thread/202#post-6456
    - https://boonsuan.github.io/erdos202.pdf
    - https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P202/Proof.lean
    - https://raw.githubusercontent.com/Shashi456/erdos-formalizations/refs/heads/main/Erdos/P202/Proof.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos204
  epc: https://www.erdosproblems.com/204
  author:
    informal:
      human: Sarosh Adenwalla
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/2501.15170
  url:
    - https://www.erdosproblems.com/forum/thread/204#post-4790
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem204.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/204.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos205
  epc: https://www.erdosproblems.com/205
  author:
    informal:
      human:
        - Wouter van Doorn
        - Terence Tao
        - Boris Alexeev
      AI: ChatGPT
    formal:
      AI:
        - ChatGPT
        - Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/205
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos205.md
  version: "4.24.0"
  todo: Import PNT+ project.

- key: ErdosProblems.Erdos206
  epc: https://www.erdosproblems.com/206
  author:
    informal:
      human: Vjekoslav Kovač
    formal:
      AI: Aristotle
      human: Matteo Del Vecchio
  arxiv: https://arxiv.org/abs/2406.07218
  url:
    - https://www.erdosproblems.com/forum/thread/206#post-5989
    - https://gist.githubusercontent.com/madeve-unipi/0920783513a1a00af4a14660852df60e/raw/522569070c2ec3a0fc7d8dfd7f95f3de2b2e3103/Erdos206.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos209
  epc: https://www.erdosproblems.com/209
  author:
    informal:
      human: Juan García Escudero
    formal:
      AI: AxiomProver
  url:
    - https://www.erdosproblems.com/forum/thread/209#post-7065
    - https://github.com/AxiomMath/erdos-public/blob/3ccf48c78b9df4aa26e1b2f90058bdd3f61da1ab/Erdos/Erdos209/solution.lean
  version: "4.27.0"

- key: ErdosProblems.Erdos210
  epc: https://www.erdosproblems.com/210
  author:
    informal:
      human:
        - L. M. Kelly
        - W. O. J. Moser
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos210.md
  version: "4.33.0"

- key: ErdosProblems.Erdos211
  epc: https://www.erdosproblems.com/211
  author:
    informal:
      human:
        - József Beck
        - Endre Szemerédi
        - William T. Trotter Jr.
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos211.md
  version: "4.33.0"

- key: ErdosProblems.Erdos214
  epc: https://www.erdosproblems.com/214
  author:
    informal:
      human: Rozália Juhász
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/214#post-4547
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem214FourPoints.lean
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem214TwelvePoints.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos215
  epc: https://www.erdosproblems.com/215
  author:
    informal:
      human:
        - Steve Jackson
        - R. Daniel Mauldin
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos215.md
  version: "4.33.0"

- key: ErdosProblems.Erdos219
  epc: https://www.erdosproblems.com/219
  author:
    informal:
      human:
        - Ben Green
        - Terence Tao
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos219.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/219.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos220
  epc: https://www.erdosproblems.com/220
  author:
    informal:
      human:
        - Hugh Montgomery
        - Robert Vaughan
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos220.md
  version: "4.33.0"

- key: ErdosProblems.Erdos221
  epc: https://www.erdosproblems.com/221
  author:
    informal:
      human:
        - Imre Ruzsa
        - Wouter van Doorn
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/221#post-3991
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem221.lean
    - https://www.cambridge.org/core/services/aop-cambridge-core/content/view/802ABD868A907C2ADB78C580C73C86FC/S0008439500061348a.pdf/on-a-problem-of-p-erdos.pdf
  version: "4.24.0"

- key: ErdosProblems.Erdos223
  epc: https://www.erdosproblems.com/223
  author:
    informal:
      human:
        - Konrad J. Swanepoel
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos223.md
  version: "4.33.0"

- key: ErdosProblems.Erdos224
  epc: https://www.erdosproblems.com/224
  author:
    informal:
      human:
        - Ludwig Danzer
        - Branko Grünbaum
    formal:
      AI:
        - GPT-5.2 Thinking
        - Codex
      human: Coder-Osman
  url:
    - https://www.erdosproblems.com/forum/thread/224#post-3157
    - https://github.com/SpringSense-Innovation-Institute/ai-for-math-lean/blob/main/erdos-problems/erdos224/Erdos224.lean
  version: "4.25.0"

- key: ErdosProblems.Erdos225
  epc: https://www.erdosproblems.com/225
  author:
    informal:
      human:
        - E. B. Saff
        - T. Sheil-Small
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos225.md
  version: "4.33.0"

- key: ErdosProblems.Erdos226
  epc: https://www.erdosproblems.com/226
  author:
    informal:
      human:
        - K. F. Barth
        - W. J. Schneider
      AI: ChatGPT
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/226
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos226.md
  version: "4.24.0"

- key: ErdosProblems.Erdos227
  epc: https://www.erdosproblems.com/227
  author:
    informal:
      human:
        - J. Clunie
        - W. K. Hayman
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos227.md
  version: "4.33.0"

- key: ErdosProblems.Erdos228
  epc: https://www.erdosproblems.com/228
  author:
    informal:
      human:
        - Paul Balister
        - Béla Bollobás
        - Robert Morris
        - Julian Sahasrabudhe
        - Marius Tiba
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos228.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/228.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos229
  epc: https://www.erdosproblems.com/229
  author:
    informal:
      human:
        - K. F. Barth
        - W. J. Schneider
      AI: ChatGPT
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/229
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos229.md
  version: "4.24.0"

- key: ErdosProblems.Erdos230
  epc: https://www.erdosproblems.com/230
  author:
    informal:
      human:
        - Jean-Pierre Kahane
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos230.md
  version: "4.33.0"

- key: ErdosProblems.Erdos231
  epc: https://www.erdosproblems.com/231
  author:
    informal:
      human:
        - Nicolaas Govert de Bruijn
        - Paul Erdős
    formal:
      AI: AxiomProver
  url:
    - https://www.erdosproblems.com/forum/thread/231#post-4320
    - https://github.com/AxiomMath/erdos-public/blob/3ccf48c78b9df4aa26e1b2f90058bdd3f61da1ab/Erdos/Erdos231/solution.lean
  version: "4.27.0"

- key: ErdosProblems.Erdos235
  epc: https://www.erdosproblems.com/235
  author:
    informal:
      human:
        - Christopher Hooley
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos235.md
  version: "4.33.0"

- key: ErdosProblems.Erdos237
  epc: https://www.erdosproblems.com/237
  author:
    informal:
      human:
        - Yong-Gao Chen
        - Yuchen Ding
    formal:
      AI: Aristotle
      human: Pietro Monticone
  arxiv: https://arxiv.org/abs/2201.10727
  url:
    - https://www.erdosproblems.com/forum/thread/237#post-5240
    - https://gist.githubusercontent.com/pitmonticone/8ea0d1cdb963b6213ac639b11d33f811/raw/98a5824d16da14313f65d77eeab5563dd874613a/Erdos237.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos237b
  epc: https://www.erdosproblems.com/237
  author:
    informal:
      human:
        - Yong-Gao Chen
        - Yuchen Ding
    formal:
      AI:
        - Aristotle
        - Codex
      human: Pietro Monticone
  url:
    - https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos237b.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos239
  epc: https://www.erdosproblems.com/239
  author:
    informal:
      human:
        - Eduard Wirsing
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos239.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/239.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos245
  epc: https://www.erdosproblems.com/245
  author:
    informal:
      human:
        - Gregory Freiman
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos245.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/245.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos246
  epc: https://www.erdosproblems.com/246
  author:
    informal:
      human: Bryan John Birch
      AI: ChatGPT
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/246
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos246.md
  version: "4.24.0"

- key: ErdosProblems.Erdos248
  epc: https://www.erdosproblems.com/248
  author:
    informal:
      human:
        - Terence Tao
        - Joni Teräväinen
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos248.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/248.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos250
  epc: https://www.erdosproblems.com/250
  author:
    informal:
      human:
        - Yuri Nesterenko
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos250.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/250.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos253
  epc: https://www.erdosproblems.com/253
  author:
    informal:
      human:
        - J. W. S. Cassels
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos253.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/253.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos255
  epc: https://www.erdosproblems.com/255
  author:
    informal:
      human:
        - Wolfgang M. Schmidt
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos255.md
  version: "4.33.0"

- key: ErdosProblems.Erdos258
  epc: https://www.erdosproblems.com/258
  author:
    informal:
      AI: GPT-5.4 Pro
      human: Przemek Chojecki
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human:
        - Przemek Chojecki
        - Stefano Rocca
  url:
    - https://www.erdosproblems.com/forum/thread/258
    - https://www.ulam.ai/research/erdos258.pdf
    - https://www.ulam.ai/research/erdos258.tar.gz
    - https://gist.githubusercontent.com/ster-oc/2b7adcf9d753cf6e29d782f7374cc57e/raw/689a8483895cbe147634dfbf2d7b1db93a3b5b5f/Erdos258.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/258.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos258b
  epc: https://www.erdosproblems.com/258
  author:
    informal:
      AI: GPT-5.4 Pro
      human: Przemek Chojecki
    statement: Formal Conjectures authors
    formal:
      AI:
        - Aristotle
        - Codex
      human:
        - Przemek Chojecki
        - Stefano Rocca
  url:
    - https://www.erdosproblems.com/forum/thread/258
    - https://www.ulam.ai/research/erdos258.pdf
    - https://www.ulam.ai/research/erdos258.tar.gz
    - https://gist.githubusercontent.com/ster-oc/2b7adcf9d753cf6e29d782f7374cc57e/raw/689a8483895cbe147634dfbf2d7b1db93a3b5b5f/Erdos258.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/258.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos259
  epc: https://www.erdosproblems.com/259
  author:
    informal:
      human:
        - Yong-Gao Chen
        - Imre Z. Ruzsa
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Stefano Rocca
  url:
    - https://www.erdosproblems.com/forum/thread/259#post-5683
    - https://gist.githubusercontent.com/ster-oc/c7429943f6b3a634797dc8b2a3b01f2d/raw/8c6b5b7f08021f0aed2312542dd2e9ee7beaa6d6/Erdos259.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/259.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos260
  epc: https://www.erdosproblems.com/260
  author:
    informal:
      human: Han Wang
      AI: GPT-5.5
    formal:
      human: Han Wang
      AI:
        - GPT-5.5
        - GPT-5.6
  arxiv: https://arxiv.org/abs/2606.24972v2
  url:
    - https://www.erdosproblems.com/forum/thread/260/proof-claims#proof-claim-77
    - https://github.com/Hanziwww/erdos260/tree/ba33ea2d16682e5811f15549018795307b97be08
  version: "4.32.0"

- key: ErdosProblems.Erdos262
  epc: https://www.erdosproblems.com/262
  author:
    informal:
      human:
        - Jaroslav Hančl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos262.md
  version: "4.33.0"

- key: ErdosProblems.Erdos264b
  partial: yes
  epc: https://www.erdosproblems.com/264
  author:
    informal:
      human:
        - Vjekoslav Kovač
        - Terence Tao
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human:
        - Pietro Monticone
        - Vjekoslav Kovač
  arxiv: https://arxiv.org/abs/2406.17593
  url:
    - https://www.erdosproblems.com/forum/thread/264#post-2258
    - https://www.erdosproblems.com/forum/thread/264#post-2236
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos264.md
    - https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos264.lean
    - https://web.math.pmf.unizg.hr/~vjekovac/EP/EP264/Erdos264_blueprint.tex
    - https://web.math.pmf.unizg.hr/~vjekovac/EP/EP264/Erdos264_converted.pdf
    - https://github.com/VjekoKovac/erdosproblems/blob/main/Erdos264.lean
    - https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos264b.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/264.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos266
  epc: https://www.erdosproblems.com/266
  author:
    informal:
      human:
        - Vjekoslav Kovač
        - Terence Tao
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos266.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/266.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos267
  epc: https://www.erdosproblems.com/267
  author:
    informal:
      human: Colin Snyder
      AI: GPT-5.6
    formal:
      human: Colin Snyder
      AI: GPT-5.6
  url:
    - https://www.erdosproblems.com/forum/thread/267/proof-claims#proof-claim-29
    - https://www.starfleetmath.com/solutions/688c4c2a-dc90-40b1-9501-c82eeb3a42e5
    - https://www.starfleetmath.com/downloads/verify/erdos-267/erdos-267-solution.zip
  version: 4.31.0
- key: ErdosProblems.Erdos268
  epc: https://www.erdosproblems.com/268
  author:
    informal:
      human: Vjekoslav Kovač
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Matteo Del Vecchio
  arxiv: https://arxiv.org/abs/2405.07681
  url:
    - https://www.erdosproblems.com/forum/thread/268#post-5359
    - https://gist.githubusercontent.com/madeve-unipi/62a8f68cdb4864b85b81a6752dcb0aa4/raw/5793aaa51089c25c37d8d63f60540367f6abe506/Erdos268.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/268.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos270
  epc: https://www.erdosproblems.com/270
  author:
    informal:
      human:
        - T. Crmarić
        - Vjekoslav Kovač
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos270.md
  version: "4.33.0"

- key: ErdosProblems.Erdos275
  epc: https://www.erdosproblems.com/275
  author:
    informal:
      human:
        - John Selfridge
        - Richard B. Crittenden
        - Charles Vanden Eynden
        - Paul Balister
        - Béla Bollobás
        - Robert Morris
        - Julian Sahasrabudhe
        - Marius Tiba
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/275
    - https://www.ams.org/journals/proc/1970-024-03/S0002-9939-1970-0258719-2/home.html
    - https://link.springer.com/article/10.1007/s10474-019-00980-z
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos275.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/275.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos277
  epc: https://www.erdosproblems.com/277
  author:
    informal:
      human:
        - J. A. Haight
        - Michael Filaseta
        - Kevin Ford
        - Sergei Konyagin
        - Carl Pomerance
        - Gang Yu
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos277.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/277.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos280
  epc: https://www.erdosproblems.com/280
  author:
    informal:
      human: Stijn Cambie
    formal:
      AI: Aristotle
      human: Lorenzo Luccioli
  url:
    - https://www.erdosproblems.com/forum/thread/280#post-5595
    - https://gist.githubusercontent.com/LorenzoLuccioli/2dda92a192c15c24263c8a258979e7e3/raw/b9f4c664a42977075e361da17759bd0f71998ff8/Erdos280.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos281
  epc: https://www.erdosproblems.com/281
  author:
    informal:
      human: Neel Somani
      AI: GPT-5.2 Pro
    formal:
      AI:
        - Aristotle
        - Gemini 3.0 Flash
      human: JakeMallen
  url:
    - https://www.erdosproblems.com/forum/thread/281#post-3445
    - https://chatgpt.com/share/696ac45b-70d8-8003-9ca4-320151e0816e
  url_ref: JakeMallen_281
  version: "4.24.0"

- key: ErdosProblems.Erdos283
  epc: https://www.erdosproblems.com/283
  author:
    informal:
      AI: GPT-5.5 Pro
      human: Liam Price
    statement: Formal Conjectures authors
    formal:
      AI:
        - Opus 4.7
        - GPT-5.5 Pro
      human: Pawan Sasanka Ammanamanchi
  url:
    - https://www.erdosproblems.com/forum/thread/283#post-6290
    - https://www.overleaf.com/read/gdmnffbshxsq#ef2000
    - https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P283/Proof_flat.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/283.lean
    - https://raw.githubusercontent.com/Shashi456/erdos-formalizations/refs/heads/main/Erdos/P283/Proof_flat.lean
  version:
    - "4.27.0"
    - "4.28.0"

- key: ErdosProblems.Erdos283b
  partial: yes
  epc: https://www.erdosproblems.com/283
  author:
    informal:
      human: Wouter van Doorn
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/283#post-260
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem283.lean
    - https://github.com/Woett/A-normal-paper-is-probably-fine/blob/main/The%20binomial%20case%20of%20Graham's%20conjecture%20on%20polynomial%20representations%20with%20prescribed%20sum%20of%20reciprocals.pdf
  version: "4.28.0"

- key: ErdosProblems.Erdos284
  epc: https://www.erdosproblems.com/284
  author:
    informal:
      human:
        - Ernest S. Croot III
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos284.md
  version: "4.33.0"

- key: ErdosProblems.Erdos285
  epc: https://www.erdosproblems.com/285
  author:
    informal:
      human:
        - Greg Martin
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos285.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/285.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos286
  epc: https://www.erdosproblems.com/286
  author:
    informal:
      human:
        - Ernest S. Croot III
        - Greg Martin
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos286.md
  version: "4.33.0"

- key: ErdosProblems.Erdos290
  epc: https://www.erdosproblems.com/290
  author:
    informal:
      human: Wouter van Doorn
    formal:
      AI: Aristotle
      human:
        - Wouter van Doorn
        - Boris Alexeev
  arxiv: https://arxiv.org/abs/2411.03073
  url:
    - https://www.erdosproblems.com/forum/thread/290#post-3180
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem290.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos291b
  partial: yes
  conditional: h_priemteller, h_bla0
  epc: https://www.erdosproblems.com/291
  author:
    informal:
      human: Wouter van Doorn
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/2411.03073
  url:
    - https://www.erdosproblems.com/forum/thread/291#post-4219
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem291.lean
    - https://github.com/Woett/Miscellaneous/blob/main/Generalized%20harmonic%20sums%20have%20arbitrarily%20large%20prime%20factors.pdf
    - https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
  version: "4.24.0"

- key: ErdosProblems.Erdos292
  epc: https://www.erdosproblems.com/292
  author:
    informal:
      human:
        - Greg Martin
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos292.md
  version: "4.33.0"

- key: ErdosProblems.Erdos294
  epc: https://www.erdosproblems.com/294
  author:
    informal:
      human:
        - Yang P. Liu
        - Mehtaab Sawhney
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos294.md
  version: "4.33.0"

- key: ErdosProblems.Erdos296
  epc: https://www.erdosproblems.com/296
  author:
    informal:
      human:
        - Thomas Bloom
        - Zachary Hunter
        - Mehtaab Sawhney
    formal:
      AI: Aristotle
      human: John Jennings
  arxiv: https://arxiv.org/abs/2112.03726
  url:
    - https://www.erdosproblems.com/forum/thread/296#post-5713
    - https://gist.githubusercontent.com/JohnEdwardJennings/d1ba8d7b8c63cc7eade1243e19e2eb35/raw/7402a8e36283841cbc7e0588760d701a4e84c3a2/Erdos296.lean
    - https://github.com/b-mehta/unit-fractions/blob/master/src/final_results.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos297
  epc: https://www.erdosproblems.com/297
  author:
    informal:
      human:
        - Yang P. Liu
        - Mehtaab Sawhney
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos297.md
  version: "4.33.0"

- key: ErdosProblems.Erdos298
  epc: https://www.erdosproblems.com/298
  author:
    informal:
      human: Thomas Bloom
    formal:
      human:
        - Bhavik Mehta
        - Thomas Bloom
  arxiv: https://arxiv.org/abs/2112.03726
  url: https://github.com/b-mehta/unit-fractions
  version: "3.42.1"

- key: ErdosProblems.Erdos299
  epc: https://www.erdosproblems.com/299
  author:
    informal:
      human: Thomas Bloom
    formal:
      human:
        - Bhavik Mehta
        - Thomas Bloom
  arxiv: https://arxiv.org/abs/2112.03726
  url: https://github.com/b-mehta/unit-fractions
  version: "3.42.1"

- key: ErdosProblems.Erdos300
  epc: https://www.erdosproblems.com/300
  author:
    informal:
      human:
        - Yang P. Liu
        - Mehtaab Sawhney
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos300.md
  version: "4.33.0"

- key: ErdosProblems.Erdos303
  epc: https://www.erdosproblems.com/303
  author:
    informal:
      human:
        - Tom C. Brown
        - Vojtěch Rödl
    statement: Formal Conjectures authors
    formal:
      AI:
        - Seed-Prover
        - Aristotle
      human:
        - Zheng Yuan
        - Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/330#post-2334
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos303.md
  version: "4.24.0"
  url_ref: Zheng_Yuan_303

- key: ErdosProblems.Erdos305
  epc: https://www.erdosproblems.com/305
  author:
    informal:
      human:
        - Michael N. Bleicher
        - Paul Erdős
        - Hisashi Yokota
        - Yang P. Liu
        - Mehtaab Sawhney
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos305.md
  version: "4.33.0"

- key: ErdosProblems.Erdos308
  epc: https://www.erdosproblems.com/308
  author:
    informal:
      human:
        - Ernest S. Croot III
        - Hisashi Yokota
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos308.md
  version: "4.33.0"

- key: ErdosProblems.Erdos309
  epc: https://www.erdosproblems.com/309
  author:
    informal:
      human:
        - Hisashi Yokota
        - Ernest S. Croot III
        - Thomas Bloom
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos309.md
  version: "4.33.0"

- key: ErdosProblems.Erdos310
  epc: https://www.erdosproblems.com/310
  author:
    informal:
      human:
        - Thomas Bloom
        - Bhavik Mehta
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos310.md
  version: "4.33.0"

- key: ErdosProblems.Erdos314
  epc: https://www.erdosproblems.com/314
  author:
    informal:
      human:
        - Jeck Lim
        - Stefan Steinerberger
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/2405.11354
  url:
    - https://www.erdosproblems.com/forum/thread/314#post-5193
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem314.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos315
  epc: https://www.erdosproblems.com/315
  author:
    informal:
      human:
        - Yuhi Kamio
        - Zheng Li
        - Quanyu Tang
    formal:
      AI: Aristotle
      human: Boris Alexeev
  arxiv:
    - https://arxiv.org/abs/2503.02317
    - https://arxiv.org/abs/2503.12277
  url:
    - https://www.erdosproblems.com/forum/thread/315
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos315.md
  version: "4.24.0"

- key: ErdosProblems.Erdos316
  epc: https://www.erdosproblems.com/316
  author:
    informal:
      human:
        - Csaba Sándor
        - Tom Stobart
    formal:
      human: Bhavik Mehta
  url: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/316.lean
  version: "4.27.0"

- key: ErdosProblems.Erdos318
  epc: https://www.erdosproblems.com/318
  author:
    informal:
      human:
        - Paul Erdős
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos318.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/318.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos320
  epc: https://www.erdosproblems.com/320
  author:
    informal:
      human:
        - Sandro Bettin
        - Loïc Grenié
        - Giuseppe Molteni
        - Carlo Sanna
      AI:
        - GPT-5.6 Sol
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos320.md
  version: "4.33.0"

- key: ErdosProblems.Erdos321
  epc: https://www.erdosproblems.com/321
  author:
    informal:
      human:
        - Sandro Bettin
        - Loïc Grenié
        - Giuseppe Molteni
        - Carlo Sanna
      AI:
        - GPT-5.6 Sol
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos321.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/321.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos327
  epc: https://www.erdosproblems.com/327
  author:
    informal:
      human:
        - Donald Della Pietra
        - Will Sawin
      AI: GPT-5.6 Sol
    formal:
      human: Donald Della Pietra
      AI: GPT-5.6 Sol
  url:
    - https://www.erdosproblems.com/forum/thread/327/proof-claims#proof-claim-168
    - https://github.com/donalddellapietra/erdos-327-proof/releases/download/proof-claim-v1/erdos-327-lean-formalization-v1.zip
    - https://github.com/donalddellapietra/erdos-327-proof/blob/5c6db2f53668edd621ec75d48821113345565ede/lean/Erdos327/Analytic/Unconditional.lean
    - https://github.com/donalddellapietra/erdos-327-proof/blob/5c6db2f53668edd621ec75d48821113345565ede/paper/main.tex
    - https://github.com/teorth/mathlib4/blob/da1f94df976c7cd38117281c57d6ee3046c8d104/Mathlib/NumberTheory/Mertens.lean
  version: "4.33.0-rc1"

- key: ErdosProblems.Erdos328
  epc: https://www.erdosproblems.com/328
  author:
    informal:
      AI: AxiomProver
    formal:
      AI: AxiomProver
  url:
    - https://www.erdosproblems.com/forum/thread/328#post-7066
    - https://github.com/AxiomMath/erdos-public/blob/3ccf48c78b9df4aa26e1b2f90058bdd3f61da1ab/Erdos/Erdos328/solution.lean
  version: "4.27.0"

- key: ErdosProblems.Erdos330
  epc: https://www.erdosproblems.com/330
  author:
    informal:
      AI: GPT-5.5 Pro
      human: David Turturean
    formal:
      AI:
        - Codex
        - GPT-5.5 Pro
      human: Allen Graham Hart
  url:
    - https://www.erdosproblems.com/forum/thread/330#post-6271
    - https://www.erdosproblems.com/forum/thread/330#post-5756
    - https://github.com/AllenGrahamHart/FormalConjectures-Bench/tree/6160036caab0dcee80395ba3beb7b6ef2731604e/formalizations/erdos330
  version: "4.27.0"

- key: ErdosProblems.Erdos331
  epc: https://www.erdosproblems.com/331
  author:
    informal:
      human: Imre Ruzsa
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/331#post-4019
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem331.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/331.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos333
  epc: https://www.erdosproblems.com/333
  author:
    informal:
      human:
        - Paul Erdős
        - Donald J. Newman
      AI: GPT-5.2 Pro
    formal:
      AI: Claude Opus 4.5
      human:
        - Liam Price
        - Kevin Barreto
  url:
    - https://www.erdosproblems.com/forum/thread/333#post-2403
    - https://chatgpt.com/s/t_69467152e8808191b9140d006994f284
    - https://chatgpt.com/s/t_694c90df3c908191a192f6233c2b14b9
  url_ref: KevinBarreto_333
  version: "4.29.1"

- key: ErdosProblems.Erdos336
  epc: https://www.erdosproblems.com/336
  author:
    informal:
      human: Colin Snyder
      AI: GPT-5.6
    formal:
      human: Colin Snyder
      AI: GPT-5.6
  url:
    - https://www.erdosproblems.com/forum/thread/336/proof-claims#proof-claim-32
    - https://www.starfleetmath.com/solutions/f1d1ef78-ae72-45c9-9990-17012d60f244
    - https://www.starfleetmath.com/downloads/verify/erdos-336/erdos-336-solution.zip
  version: 4.31.0
- key: ErdosProblems.Erdos337
  epc: https://www.erdosproblems.com/337
  author:
    informal:
      human:
        - Imre Ruzsa
        - Sándor Turjányi
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/337
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos337.md
  version: "4.24.0"

- key: ErdosProblems.Erdos339
  epc: https://www.erdosproblems.com/339
  author:
    informal:
      human:
        - Norbert Hegyvári
        - François Hennecart
        - Alain Plagne
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos339.md
  version: "4.33.0"

- key: ErdosProblems.Erdos341
  epc: https://www.erdosproblems.com/341
  author:
    informal:
      human: Zhiheng Li
      AI: GPT-5.6 Sol
    formal:
      human: Zhiheng Li
      AI: GPT-5.6 Sol
  url:
    - https://www.erdosproblems.com/forum/thread/341/proof-claims#proof-claim-200
    - https://github.com/LiAlreadyExists/Erdos-341/blob/c1d912189983ac2fa177e7adb1223d4b9ba85e6f/LeanProject/Erdos341.lean
    - https://github.com/LiAlreadyExists/Erdos-341/blob/c1d912189983ac2fa177e7adb1223d4b9ba85e6f/README.md
  version: "4.33.0-rc1"

- key: ErdosProblems.Erdos343
  epc: https://www.erdosproblems.com/343
  author:
    informal:
      human:
        - Endre Szemerédi
        - Van H. Vu
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos343.md
  version: "4.33.0"

- key: ErdosProblems.Erdos344
  epc: https://www.erdosproblems.com/344
  author:
    informal:
      human:
        - Endre Szemerédi
        - Van H. Vu
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos344.md
  version: "4.33.0"

- key: ErdosProblems.Erdos346
  epc: https://www.erdosproblems.com/346
  author:
    informal:
      human: Liam Price
      AI: GPT Pro
    formal:
      human: Liam Price
      AI: GPT-5.5 (Codex)
  url:
    - https://www.erdosproblems.com/forum/thread/346/proof-claims#proof-claim-59
    - https://www.erdosproblems.com/forum/thread/346
    - https://www.overleaf.com/read/tgrrgqpbjpht#c5a085
- key: ErdosProblems.Erdos347
  epc: https://www.erdosproblems.com/347
  author:
    informal:
      human: Enrique Barschkis
      AI: GPT Codex
    formal:
      AI: Aristotle
      human: Enrique Barschkis
  url:
    - https://www.erdosproblems.com/forum/thread/347#post-3606
    - https://github.com/ebarschkis/ErdosProblem/blob/main/Problem347/347.pdf
    - https://github.com/ebarschkis/ErdosProblem/blob/main/Problem347/note.tex
    - https://github.com/ebarschkis/ErdosProblem/blob/main/Problem347/Formalization.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos350
  epc: https://www.erdosproblems.com/350
  author:
    informal:
      human: Charles Albert Ryavec
      AI: ChatGPT
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/350
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos350.md
  version:
    - "4.20.0-rc5"
    - "4.24.0"

- key: ErdosProblems.Erdos351
  epc: https://www.erdosproblems.com/351
  author:
    informal:
      AI: GPT-5.5 Pro
      human:
        - Liam Price
        - Kevin Barreto
    statement: Formal Conjectures authors
    formal:
      AI:
        - Opus 4.7
        - GPT-5.5 Pro
      human: Pawan Sasanka Ammanamanchi
  url:
    - https://www.erdosproblems.com/forum/thread/283#post-6290
    - https://www.overleaf.com/read/gdmnffbshxsq#ef2000
    - https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P283/Proof_flat.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/351.lean
    - https://raw.githubusercontent.com/Shashi456/erdos-formalizations/refs/heads/main/Erdos/P283/Proof_flat.lean
  version:
    - "4.27.0"
    - "4.28.0"

- key: ErdosProblems.Erdos353
  epc: https://www.erdosproblems.com/353
  author:
    informal:
      human:
        - Junnosuke Koizumi
        - Vjekoslav Kovač
        - Bruno Predojević
    formal:
      AI: Aristotle
      human: JoshuaB
  url:
    - https://www.erdosproblems.com/forum/thread/353#post-7085
    - https://www.erdosproblems.com/forum/thread/353#post-7095
    - https://www.erdosproblems.com/forum/thread/353#post-7098
    - https://arxiv.org/abs/2501.01914
    - https://arxiv.org/abs/2412.11725
  url_ref:
    - JoshuaB_353_koizumi
    - JoshuaB_353_cyclic
    - JoshuaB_353_polygon
  version: "4.28.0"

- key: ErdosProblems.Erdos355
  epc: https://www.erdosproblems.com/355
  author:
    informal:
      human:
        - Wouter van Doorn
        - Vjekoslav Kovač
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/2509.24971
  url:
    - https://www.erdosproblems.com/forum/thread/355#post-4741
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem355.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/355.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos356
  epc: https://www.erdosproblems.com/356
  author:
    informal:
      human:
        - Adrian Beker
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos356.md
  version: "4.33.0"

- key: ErdosProblems.Erdos358
  epc: https://www.erdosproblems.com/358
  author:
    informal:
      human:
        - Terence Tao
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos358.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/358.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos362
  epc: https://www.erdosproblems.com/362
  author:
    informal:
      human:
        - András Sárközy
        - Endre Szemerédi
        - Gábor Halász
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos362.md
  version: "4.33.0"

- key: ErdosProblems.Erdos363
  epc: https://www.erdosproblems.com/363
  author:
    informal:
      human: Maciej Ulas
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/363#post-4709
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem363.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos367b
  partial: yes
  epc: https://www.erdosproblems.com/367
  author:
    informal:
      human:
        - Wouter van Doorn
        - Terence Tao
      AI: Gemini Deepthink
    statement:
      human: Boris Alexeev
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/367#post-1766
    - https://www.erdosproblems.com/forum/thread/367#post-1776
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos367.md
    - https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos367.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos368b
  partial: yes
  epc: https://www.erdosproblems.com/368
  author:
    informal:
      human: Georg Pólya
      AI: ChatGPT
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/368#post-4335
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos368.md
    - https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos368b.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos369
  epc: https://www.erdosproblems.com/369
  author:
    informal:
      human: Sky Yang
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/369#post-5058
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem369.lean
    - https://drive.google.com/file/d/1MxgrA2haXKv_NKSa7sqUI2hZYyZ5JmfP/view
  version: "4.28.0"

- key: ErdosProblems.Erdos370
  epc: https://www.erdosproblems.com/370
  author:
    informal:
      human: Stefan Steinerberger
      AI: ChatGPT 5.1 Pro
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/370
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos370.md
  version:
    - "4.20.0-rc5"
    - "4.24.0"

- key: ErdosProblems.Erdos372
  epc: https://www.erdosproblems.com/372
  author:
    informal:
      human:
        - Sungjin Kim
        - James Maynard
        - Terence Tao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos372.md
  version: "4.33.0"

- key: ErdosProblems.Erdos378
  epc: https://www.erdosproblems.com/378
  author:
    informal:
      human:
        - Andrew Granville
        - Olivier Ramaré
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos378.md
  version: "4.33.0"

- key: ErdosProblems.Erdos379
  epc: https://www.erdosproblems.com/379
  author:
    informal:
      human:
        - Stijn Cambie
        - Vjekoslav Kovač
        - Terence Tao
    formal:
      AI: Seed-Prover 1.5
      human: Zheng Yuan
  url: https://www.erdosproblems.com/forum/thread/379#post-2350
  version: "4.22.0"
  url_ref: Zheng_Yuan_379

- key: ErdosProblems.Erdos384
  epc: https://www.erdosproblems.com/384
  author:
    informal:
      human:
        - E. F. Ecklund Jr.
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos384.md
  version: "4.33.0"

- key: ErdosProblems.Erdos387
  epc: https://www.erdosproblems.com/387
  author:
    informal:
      human:
        - Hung M. Bui
        - S. Naprienko
        - Kyle Pratt
        - Alexandru Zaharescu
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos387.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/387.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos391
  epc: https://www.erdosproblems.com/391
  author:
    informal:
      human:
        - Boris Alexeev
        - John H. Conway
        - Michael Rosenfeld
        - Andrew Sutherland
        - Terence Tao
        - Michael Uhr
        - Kevin Ventullo
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos391.md
  version: "4.33.0"

- key: ErdosProblems.Erdos392
  epc: https://www.erdosproblems.com/392
  author:
    informal:
      human:
        - Stijn Cambie
        - Terence Tao
    formal:
      AI: Aristotle
      human:
        - Terence Tao
        - Pietro Monticone
        - Alex Kontorovich
  arxiv: https://arxiv.org/abs/2503.20170
  url:
    - https://www.erdosproblems.com/forum/thread/392#post-4410
    - https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/Erdos392.lean
    - https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint/sect0009.html#a0000000039
  version: "4.28.0"
  todo: Import PNT+ project.

- key: ErdosProblems.Erdos394
  epc: https://www.erdosproblems.com/394
  author:
    informal:
      human: Colin Snyder
      AI: GPT-5.6
    formal:
      human: Colin Snyder
      AI: GPT-5.6
  url:
    - https://www.erdosproblems.com/forum/thread/394/proof-claims#proof-claim-33
    - https://www.starfleetmath.com/solutions/188c4e29-f0bb-4975-8f1d-b0a31c5fcd2e
    - https://www.starfleetmath.com/downloads/verify/erdos-394/erdos-394-solution.zip
  version: "4.31.0"

- key: ErdosProblems.Erdos395
  epc: https://www.erdosproblems.com/395
  author:
    informal:
      human:
        - Xiaoyu He
        - Tomasz Juškevičius
        - Bhargav Narayanan
        - Sam Spiro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos395.md
  version: "4.33.0"

- key: ErdosProblems.Erdos397
  epc: https://www.erdosproblems.com/397
  author:
    informal:
      AI: GPT-5.2 Pro
      human: Neel Somani
    formal:
      AI: Aristotle
      human: Lawrence Wu
  url:
    - https://www.erdosproblems.com/forum/thread/397#post-2940
    - https://www.erdosproblems.com/forum/thread/397#post-2936
    - https://gist.githubusercontent.com/llllvvuu/40d68cfa9de9f43eece07ff4fdc3b0ef/raw/966750065320fe126fbe5a8a7ea50439d7519c6c/397.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos399
  epc: https://www.erdosproblems.com/399
  author:
    informal:
      human: Jonas Barfield
    formal:
      AI: Codex
      human: Cong Lu
  url: https://github.com/google-deepmind/formal-conjectures/commit/ce390075c49403db77b955a3f3a8bf4c4de99cbe
  version: "4.22.0"

- key: ErdosProblems.Erdos401
  epc: https://www.erdosproblems.com/401
  author:
    informal:
      AI: GPT-5.2 Pro
      human:
        - Kevin Barreto
        - Liam Price
    formal:
      AI: Aristotle
      human:
        - Kevin Barreto
        - Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/401#post-2977
    - https://www.erdosproblems.com/forum/thread/401#post-3002
    - https://chatgpt.com/s/t_6963cf5fca208191a220cf21965a12e8
    - https://drive.google.com/file/d/1SY_LjPToevYaFl5eNl-rUxJrjrP5u4RC/view
    - https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos401b.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos402
  epc: https://www.erdosproblems.com/402
  author:
    informal:
      human:
        - R. Balasubramanian
        - K. Soundararajan
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos402.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/402.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos403
  epc: https://www.erdosproblems.com/403
  author:
    informal:
      AI: AxiomProver
    formal:
      AI: AxiomProver
  url:
    - https://www.erdosproblems.com/forum/thread/403#post-7067
    - https://github.com/AxiomMath/erdos-public/blob/3ccf48c78b9df4aa26e1b2f90058bdd3f61da1ab/Erdos/Erdos403/solution.lean
  version: "4.27.0"

- key: ErdosProblems.Erdos405
  epc: https://www.erdosproblems.com/405
  author:
    informal:
      human:
        - Béla Brindza
        - Paul Erdős
        - Kunrui Yu
        - Dehua Liu
        - Maohua Le
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos405.md
  version: "4.33.0"

- key: ErdosProblems.Erdos407
  epc: https://www.erdosproblems.com/407
  author:
    informal:
      human:
        - Prajeet Bajpai
        - Michael A. Bennett
        - Jan-Hendrik Evertse
        - Kálmán Győry
        - Carl Ludwig Stewart
        - Robert Tijdeman
        - Hans Peter Schlickewei
        - Wolfgang M. Schmidt
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos407.md
  version: "4.33.0"

- key: ErdosProblems.Erdos418
  epc: https://www.erdosproblems.com/418
  author:
    informal:
      human:
        - Jerzy Browkin
        - Andrzej Schinzel
      AI: ChatGPT 5.1 Pro
    statement:
      human:
        - Formal Conjectures authors
        - Salvatore Mercuri
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/418
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos418.md
  version:
    - "4.20.0-rc5"
    - "4.24.0"

- key: ErdosProblems.Erdos419
  epc: https://www.erdosproblems.com/419
  author:
    informal:
      human:
        - Paul Erdős
        - S. W. Graham
        - Aleksandar Ivić
        - Carl Pomerance
        - Mehtaab Sawhney
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/419
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos419.md
  version: "4.24.0"

- key: ErdosProblems.Erdos424
  epc: https://www.erdosproblems.com/424
  author:
    informal:
      AI: ChatGPT 5.6 Pro
      human: Samuel Korsky
    formal:
      AI: Codex
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/424/proof-claims#proof-claim-91
    - https://drive.google.com/file/d/1SGSUQhNB8KL75VPqdfAq9yzFNEYL6Mwn/view
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/424.lean
  version: "4.32.0"

- key: ErdosProblems.Erdos426
  epc: https://www.erdosproblems.com/426
  author:
    informal:
      human:
        - Domagoj Bradač
        - Micha Christoph
    formal:
      AI: Aristotle
      human: Lorenzo Luccioli
  url:
    - https://www.erdosproblems.com/forum/thread/426#post-5643
    - https://www.erdosproblems.com/forum/thread/426#post-5775
    - https://gist.githubusercontent.com/LorenzoLuccioli/7c10c6803e56a3271ca6ebfc9cfb89ad/raw/9aa347c235591c53684d9ac06050c18b183aea23/Erdos426.lean
    - https://gist.githubusercontent.com/LorenzoLuccioli/6740274ef8c8bd77a6c966887a72b198/raw/656e1c8330a75a6fd003efef2a8bcae1966482df/Erdos426.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos427
  epc: https://www.erdosproblems.com/427
  author:
    informal:
      human:
        - Cedric Pilatte
        - D. K. L. Shiu
    formal:
      AI: Aristotle
      human: John Jennings
  url:
    - https://www.erdosproblems.com/forum/thread/427#post-5920
    - https://gist.githubusercontent.com/JohnEdwardJennings/e2c6ef0daab55857b7cc9d340de7af84/raw/8ff97800e38582c71246a238e7541a9d69488cbd/Erdos427.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos429
  epc: https://www.erdosproblems.com/429
  author:
    informal:
      human: Desmond Weisenberg
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/429#post-3910
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem429.lean
    - https://math.colgate.edu/~integers/y89/y89.pdf
  version: "4.24.0"

- key: ErdosProblems.Erdos433
  epc: https://www.erdosproblems.com/433
  author:
    informal:
      human: Jacques Dixmier
    formal:
      AI:
        - Gemini 3.1 Pro
        - Gemini 3.0 Flash
        - Claude Sonnet 4.6
        - Project Numina
        - Aristotle
        - ulam.ai cli harness
      human: JoshuaB
  url:
    - https://www.erdosproblems.com/forum/thread/433#post-4436
    - https://github.com/YaelDillies/MiscYD/blob/master/MiscYD/AddCombi/Kneser/Kneser.lean
  url_ref: JoshuaB_433
  version: "4.24.0"

- key: ErdosProblems.Erdos434
  epc: https://www.erdosproblems.com/434
  author:
    informal:
      human:
        - Jacques Dixmier
        - G. Kiss
    formal:
      AI: Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/434#post-4437
  url_ref: JoshuaB_434
  version: "4.24.0"

- key: ErdosProblems.Erdos435
  epc: https://www.erdosproblems.com/435
  author:
    informal:
      human:
        - W. Hwang
        - K. Song
        - Peake
        - Stijn Cambie
    formal:
      AI: Aristotle
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/2412.17882
  url:
    - https://www.erdosproblems.com/forum/thread/435
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos435.md
  version: "4.24.0"

- key: ErdosProblems.Erdos437
  epc: https://www.erdosproblems.com/437
  author:
    informal:
      human:
        - Hung M. Bui
        - Kyle Pratt
        - Alexandru Zaharescu
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos437.md
  version: "4.33.0"

- key: ErdosProblems.Erdos438
  epc: https://www.erdosproblems.com/438
  author:
    informal:
      human:
        - A. Khalfalah
        - S. Lodha
        - Endre Szemerédi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos438.md
  version: "4.33.0"

- key: ErdosProblems.Erdos439
  epc: https://www.erdosproblems.com/439
  author:
    informal:
      human:
        - A. Khalfalah
        - S. Lodha
        - Endre Szemerédi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos439.md
  version: "4.33.0"

- key: ErdosProblems.Erdos440
  epc: https://www.erdosproblems.com/440
  author:
    informal:
      human:
        - Paul Erdős
        - Endre Szemerédi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos440.md
  version: "4.33.0"

- key: ErdosProblems.Erdos441
  epc: https://www.erdosproblems.com/441
  author:
    informal:
      human:
        - Yong-Gao Chen
        - Li-Xia Dai
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos441.md
  version: "4.33.0"

- key: ErdosProblems.Erdos442
  epc: https://www.erdosproblems.com/442
  author:
    informal:
      human:
        - Terence Tao
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos442.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/442.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos443
  epc: https://www.erdosproblems.com/443
  author:
    informal:
      human:
        - N. Hegyvári
        - Stijn Cambie
    formal:
      AI: Aristotle
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/2503.24201
  url:
    - https://www.erdosproblems.com/forum/thread/443
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos443.md
  version: "4.24.0"

- key: ErdosProblems.Erdos444
  epc: https://www.erdosproblems.com/444
  author:
    informal:
      human:
        - Paul Erdős
        - András Sárközy
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos444.md
  version: "4.33.0"

- key: ErdosProblems.Erdos446
  epc: https://www.erdosproblems.com/446
  author:
    informal:
      human:
        - Kevin Ford
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos446.md
  version: "4.33.0"

- key: ErdosProblems.Erdos447
  epc: https://www.erdosproblems.com/447
  author:
    informal:
      human: Daniel Kleitman
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/447
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos447.md
  version: "4.24.0"

- key: ErdosProblems.Erdos448
  epc: https://www.erdosproblems.com/448
  author:
    informal:
      human:
        - Paul Erdős
        - Gérald Tenenbaum
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos448.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/448.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos449
  epc: https://www.erdosproblems.com/449
  author:
    informal:
      human:
        - Kevin Ford
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos449.md
  version: "4.33.0"

- key: ErdosProblems.Erdos453
  epc: https://www.erdosproblems.com/453
  author:
    informal:
      human: Carl Pomerance
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/453
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos453.md
  version: "4.24.0"

- key: ErdosProblems.Erdos457
  epc: https://www.erdosproblems.com/457
  author:
    informal:
      AI: GPT-5.2 Pro
      human: Kevin Barreto
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/457#post-4668
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem457.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/457.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos459
  epc: https://www.erdosproblems.com/459
  author:
    informal:
      human: Stijn Cambie
    formal:
      AI: Aristotle
      human:
        - Boris Alexeev
        - Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/459#post-4716
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem459.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos464
  epc: https://www.erdosproblems.com/464
  author:
    informal:
      human: Bernard de Mathan
    formal:
      AI: Aristotle
      human: JoshuaB
  url:
    - https://www.erdosproblems.com/forum/thread/464#post-7120
    - https://aristotle.harmonic.fun/dashboard/requests/f9894d2d-4bb1-42da-9301-e508aa881b17
  version: "4.28.0"

- key: ErdosProblems.Erdos465
  epc: https://www.erdosproblems.com/465
  author:
    informal:
      human:
        - Sergei V. Konyagin
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos465.md
  version: "4.33.0"

- key: ErdosProblems.Erdos466
  epc: https://www.erdosproblems.com/466
  author:
    informal:
      human:
        - Ronald Graham
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos466.md
  version: "4.33.0"

- key: ErdosProblems.Erdos469
  epc: https://www.erdosproblems.com/469
  author:
    informal:
      AI:
        - GPT-5.6 Sol Ultra (OpenAI Codex)
        - Anthropic Claude Fable 5
      human: Zachary J. Lewis
    formal:
      AI: GPT-5.6 Sol Ultra (OpenAI Codex)
      human: Zachary J. Lewis
  url:
    - https://www.erdosproblems.com/forum/thread/469/proof-claims#proof-claim-2
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem469.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos471
  epc: https://www.erdosproblems.com/471
  author:
    informal:
      human:
        - Luka Mrazović
        - Vjekoslav Kovač
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos471.md
  version: "4.33.0"

- key: ErdosProblems.Erdos473
  epc: https://www.erdosproblems.com/473
  author:
    informal:
      human:
        - A. M. Odlyzko
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos473.md
  version: "4.33.0"

- key: ErdosProblems.Erdos476
  epc: https://www.erdosproblems.com/476
  author:
    informal:
      human:
        - J. A. Dias da Silva
        - Yahya Ould Hamidoune
        - Noga Alon
        - Melvyn B. Nathanson
        - Imre Z. Ruzsa
      AI: ChatGPT
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/476
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos476.md
  version: "4.24.0"

- key: ErdosProblems.Erdos480
  epc: https://www.erdosproblems.com/480
  author:
    informal:
      human:
        - Fan Chung
        - Ronald Graham
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos480.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/480.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos481
  epc: https://www.erdosproblems.com/481
  author:
    informal:
      human: Kevin Barreto
    formal:
      AI: Claude Opus 4.5
      human: Kevin Barreto
  url: https://www.erdosproblems.com/forum/thread/481#post-1930
  url_ref: KevinBarreto_481
  version: "4.29.1"

- key: ErdosProblems.Erdos482
  epc: https://www.erdosproblems.com/482
  author:
    informal:
      human:
        - R. L. Graham
        - H. O. Pollak
        - G. Rabinowitz
        - E. Gilbert
        - Thomas Stoll
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos482.md
  version: "4.33.0"

- key: ErdosProblems.Erdos484
  epc: https://www.erdosproblems.com/484
  author:
    informal:
      human:
        - Paul Erdős
        - András Sárközy
        - Vera T. Sós
    formal:
      AI: Aristotle
      human: Tomaz Mascarenhas
  url: https://www.erdosproblems.com/forum/thread/484#post-5448
  url_ref: tomaz1502_484
  version: "4.28.0"

- key: ErdosProblems.Erdos485
  epc: https://www.erdosproblems.com/485
  author:
    informal:
      human:
        - Andrzej Schinzel
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos485.md
  version: "4.33.0"

- key: ErdosProblems.Erdos485b
  partial: yes
  epc: https://www.erdosproblems.com/485
  author:
    informal:
      human: W. Verdenius
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/485#post-4030
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem485.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos486
  epc: https://www.erdosproblems.com/486
  author:
    informal:
      human: Shouqiao Wang
      AI: GPT-5.6 Sol
    formal:
      human: Shouqiao Wang
  url:
    - https://www.erdosproblems.com/forum/thread/486/proof-claims#proof-claim-63
    - https://github.com/ShouqiaoW/erdos/tree/bb8d6cf6180e3abbe67fc5b01ac1c0efa2f2d0fe/486/lean
    - https://github.com/ShouqiaoW/erdos/tree/d28713ac8245ca86a686b8c67370a8d19d81b242/486/lean
    - https://github.com/ShouqiaoW/erdos/blob/d28713ac8245ca86a686b8c67370a8d19d81b242/486/paper.pdf
  version: 4.27.0
- key: ErdosProblems.Erdos487
  epc: https://www.erdosproblems.com/487
  author:
    informal:
      human: Daniel Kleitman
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/487
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos487.md
  version: "4.24.0"

- key: ErdosProblems.Erdos489
  epc: https://www.erdosproblems.com/489
  author:
    informal:
      human: Colin Snyder
      AI: GPT-5.6
    formal:
      human: Colin Snyder
      AI: GPT-5.6
  url:
    - https://www.erdosproblems.com/forum/thread/489/proof-claims#proof-claim-36
    - https://www.starfleetmath.com/solutions/e5d1c3ca-0e42-4e89-84cc-31a603f56468
    - https://www.starfleetmath.com/downloads/verify/erdos-489/erdos-489-solution.zip
  version: 4.31.0
- key: ErdosProblems.Erdos490
  epc: https://www.erdosproblems.com/490
  author:
    informal:
      human: Endre Szemerédi
      AI: ChatGPT 5.5 Pro
    formal:
      AI:
        - Aristotle
        - Codex
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/490#post-6497
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem490.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos492
  epc: https://www.erdosproblems.com/492
  author:
    informal:
      human:
        - Wolfgang M. Schmidt
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos492.md
  version: "4.33.0"

- key: ErdosProblems.Erdos493
  epc: https://www.erdosproblems.com/493
  author:
    formal:
      AI:
        - Seed-Prover 1.5
        - Aristotle
        - ChatGPT
      human: Zheng Yuan
  url:
    - https://www.erdosproblems.com/forum/thread/493
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos493.md
  version: "4.24.0"

- key: ErdosProblems.Erdos494
  epc: https://www.erdosproblems.com/494
  author:
    informal:
      human:
        - Basil Gordon
        - Aviezri S. Fraenkel
        - Ernst G. Straus
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos494.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/494.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos496
  epc: https://www.erdosproblems.com/496
  author:
    informal:
      human:
        - Grigory Margulis
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos496.md
  version: "4.33.0"

- key: ErdosProblems.Erdos497
  epc: https://www.erdosproblems.com/497
  author:
    informal:
      human: Daniel Kleitman
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/497
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos497.md
  version: "4.24.0"

- key: ErdosProblems.Erdos498
  epc: https://www.erdosproblems.com/498
  author:
    informal:
      human: Daniel J. Kleitman
    formal:
      AI:
        - Gemini Flash
        - Gemini Pro
        - Claude Opus
        - Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/498#post-3844
  url_ref: JoshuaB_498
  version: "4.24.0"

- key: ErdosProblems.Erdos499
  epc: https://www.erdosproblems.com/499
  author:
    informal:
      human:
        - Marvin Marcus
        - Henryk Minc
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/499
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos499.md
  version: "4.24.0"

- key: ErdosProblems.Erdos501
  epc: https://www.erdosproblems.com/501
  author:
    informal:
      human:
        - Elliot Glazer
        - Stephen H. Hechler
        - Ludomir Newelski
        - Janusz Pawlikowski
        - Wiesław Seredyński
      AI:
        - GPT-5.6 Sol
    statement: Formal Conjectures authors; Elliot Glazer and Claude Fable 5
    formal:
      human:
        - Elliot Glazer
      AI:
        - Claude Fable 5
        - Claude Opus 4.8
  url:
    - https://www.erdosproblems.com/forum/thread/501/proof-claims#proof-claim-207
    - https://github.com/elliotglazer/erdos501/tree/218d1c1e46f77d4db80e566d1721782e85b94a17
    - https://github.com/elliotglazer/erdos501/blob/218d1c1e46f77d4db80e566d1721782e85b94a17/formalization.yaml
  version: "4.34.0-rc1"

- key: ErdosProblems.Erdos502
  epc: https://www.erdosproblems.com/502
  author:
    informal:
      human:
        - Fedor Petrov
        - Cosmin Pohoata
    formal:
      AI: Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/502#post-4106
  url_ref: JoshuaB_502
  version: "4.24.0"

- key: ErdosProblems.Erdos505
  epc: https://www.erdosproblems.com/505
  author:
    informal:
      human:
        - Jeff Kahn
        - Gil Kalai
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/505
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos505.md
  version: "4.24.0"

- key: ErdosProblems.Erdos506
  epc: https://www.erdosproblems.com/506
  author:
    informal:
      human:
        - P. D. T. A. Elliott
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos506.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/506.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos511
  epc: https://www.erdosproblems.com/511
  author:
    informal:
      human:
        - Christian Pommerenke
        - L. Huang
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos511.md
  version: "4.33.0"

- key: ErdosProblems.Erdos512
  epc: https://www.erdosproblems.com/512
  author:
    informal:
      human:
        - O. Carruth McGehee
        - Louis Pigno
        - Brent Smith
    formal:
      AI: Aristotle
      human: JoshuaB
  url:
    - https://www.erdosproblems.com/forum/thread/512#post-7140
    - https://aristotle.harmonic.fun/dashboard/requests/b663fac0-b653-4148-8d0a-9ae5c7dbdaea

- key: ErdosProblems.Erdos515
  epc: https://www.erdosproblems.com/515
  author:
    informal:
      human:
        - John Lewis
        - John Rossi
        - Allen Weitsman
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos515.md
  version: "4.33.0"

- key: ErdosProblems.Erdos516
  epc: https://www.erdosproblems.com/516
  author:
    informal:
      human:
        - W. H. J. Fuchs
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos516.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/516.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos518
  epc: https://www.erdosproblems.com/518
  author:
    informal:
      human:
        - Alexey Pokrovskiy
        - Leo Versteegen
        - Ella Williams
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos518.md
  version: "4.33.0"

- key: ErdosProblems.Erdos519
  epc: https://www.erdosproblems.com/519
  author:
    informal:
      human: F. V. Atkinson
    formal:
      AI: Aristotle
      human: John Jennings
  url:
    - https://www.erdosproblems.com/forum/thread/519#post-5599
    - https://gist.githubusercontent.com/JohnEdwardJennings/db1e0cb00b7d6866193c12f1c70a1813/raw/e629fcf1976d5b241d628c0b65e2b1e3701f51a6/Erdos519.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos520
  epc: https://www.erdosproblems.com/520
  author:
    informal:
      human: Sigurd William Rachlew Høystad
      AI:
        - GPT-5.6 Sol Pro
        - Claude Fable 5
    formal:
      human: Sigurd William Rachlew Høystad
      AI:
        - GPT-5.6 Sol Pro
        - Claude Fable 5
  url:
    - https://www.erdosproblems.com/forum/thread/520/proof-claims#proof-claim-183
    - https://github.com/saasom/Erdos520/tree/v1.1.0
    - https://github.com/saasom/Erdos520/blob/dea062793bf11efd962752ee378ef84720c9857e/Erdos/Problem520/Unconditional.lean
    - https://github.com/saasom/Erdos520/blob/dea062793bf11efd962752ee378ef84720c9857e/paper/erdos520_note.tex
    - https://github.com/saasom/Erdos520/blob/dea062793bf11efd962752ee378ef84720c9857e/CITATION.cff
  version: "4.30.0-rc2"

- key: ErdosProblems.Erdos523
  epc: https://www.erdosproblems.com/523
  author:
    informal:
      human:
        - Gábor Halász
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos523.md
  version: "4.33.0"

- key: ErdosProblems.Erdos525
  epc: https://www.erdosproblems.com/525
  author:
    informal:
      human:
        - Nicholas A. Cook
        - Hoi H. Nguyen
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos525.md
  version: "4.33.0"

- key: ErdosProblems.Erdos526
  epc: https://www.erdosproblems.com/526
  author:
    informal:
      human:
        - L. A. Shepp
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos526.md
  version: "4.33.0"

- key: ErdosProblems.Erdos527
  epc: https://www.erdosproblems.com/527
  author:
    informal:
      human:
        - Marcus Michelen
        - Mehtaab Sawhney
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos527.md
  version: "4.33.0"

- key: ErdosProblems.Erdos532
  epc: https://www.erdosproblems.com/532
  author:
    informal:
      human: Neil Hindman
    formal:
      human: David Wärn
  url:
    - https://www.erdosproblems.com/forum/thread/532#post-4004
    - https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Hindman.html
    - https://github.com/leanprover-community/mathlib4/blob/20c3a51ac9205f8eeb30886a4f1744a22e981ebe/Mathlib/Combinatorics/Hindman.lean
  version: "4.29.1"

- key: ErdosProblems.Erdos533
  epc: https://www.erdosproblems.com/533
  author:
    informal:
      human:
        - József Balogh
        - John Lenz
        - Hong Liu
        - Christian Reiher
        - Maryam Sharifzadeh
        - Katherine Staden
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos533.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/533.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos534
  epc: https://www.erdosproblems.com/534
  author:
    informal:
      human:
        - Rudolf Ahlswede
        - Levon H. Khachatrian
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos534.md
  version: "4.33.0"

- key: ErdosProblems.Erdos537
  epc: https://www.erdosproblems.com/537
  author:
    informal:
      human: Imre Z. Ruzsa
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/537
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos537.md
  version: "4.24.0"

- key: ErdosProblems.Erdos538
  epc: https://www.erdosproblems.com/538
  author:
    informal:
      human: Colin Snyder
      AI: GPT-5.6
    formal:
      human: Colin Snyder
      AI: GPT-5.6
  url:
    - https://www.erdosproblems.com/forum/thread/538/proof-claims#proof-claim-39
    - https://www.starfleetmath.com/solutions/c82e5d7a-dda9-411c-b02c-fc5b25e587c1
    - https://www.starfleetmath.com/downloads/verify/erdos-538/erdos-538-solution.zip
  version: 4.31.0
- key: ErdosProblems.Erdos540
  epc: https://www.erdosproblems.com/540
  author:
    informal:
      human: Endre Szemerédi
    formal:
      AI: Aristotle
      human: Matteo Del Vecchio
  url:
    - https://www.erdosproblems.com/forum/thread/540#post-5410
    - https://gist.githubusercontent.com/madeve-unipi/e5b448ddfb84f4c5427d22555f19b1e6/raw/77b2c8499a2e858e84832d72dcbe8a2e04b6a451/Erdos540.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos541
  epc: https://www.erdosproblems.com/541
  author:
    informal:
      human:
        - Paul Erdős
        - Endre Szemerédi
        - Weidong Gao
        - Yahya Ould Hamidoune
        - Guoqing Wang
        - David J. Grynkiewicz
      AI: ChatGPT
    statement: Formal Conjectures authors
    formal:
      AI:
        - Aristotle
        - ChatGPT
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/0903.3200
  url:
    - https://www.erdosproblems.com/forum/thread/541
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos541.md
  version: "4.24.0"

- key: ErdosProblems.Erdos542
  epc: https://www.erdosproblems.com/542
  author:
    informal:
      human:
        - Andrzej Schinzel
        - György Szekeres
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos542.md
  version: "4.33.0"

- key: ErdosProblems.Erdos543
  epc: https://www.erdosproblems.com/543
  author:
    informal:
      human:
        - Q. Tang
      AI:
        - ChatGPT
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos543.md
  version: "4.33.0"

- key: ErdosProblems.Erdos546
  epc: https://www.erdosproblems.com/546
  author:
    informal:
      human:
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos546.md
  version: "4.33.0"

- key: ErdosProblems.Erdos549
  epc: https://www.erdosproblems.com/549
  author:
    informal:
      human:
        - Sergey Norin
        - Yelena Sun
        - Yufei Zhao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos549.md
  version: "4.33.0"

- key: ErdosProblems.Erdos550
  epc: https://www.erdosproblems.com/550
  author:
    informal:
      human: Eric Li
      AI:
        - GPT-5.5 Pro
        - OpenAI Codex (GPT-5 family)
    formal:
      human: Eric Li
      AI:
        - Aristotle
        - OpenAI ChatGPT
        - OpenAI Codex (GPT-5 family)
  arxiv: https://arxiv.org/abs/2606.23659v2
  url:
    - https://www.erdosproblems.com/forum/thread/550/proof-claims#proof-claim-74
    - https://github.com/ericlisg/erdos550-lean/tree/6624ede70821f095eaee49865448af4e4f8c421c
    - https://github.com/ericlisg/erdos550-lean/blob/6624ede70821f095eaee49865448af4e4f8c421c/formalization.yaml
  version: "4.28.0"

- key: ErdosProblems.Erdos553
  epc: https://www.erdosproblems.com/553
  author:
    informal:
      human:
        - Noga Alon
        - Vojtěch Rödl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos553.md
  version: "4.33.0"

- key: ErdosProblems.Erdos559
  epc: https://www.erdosproblems.com/559
  author:
    informal:
      human:
        - Vojtěch Rödl
        - Endre Szemerédi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos559.md
  version: "4.33.0"

- key: ErdosProblems.Erdos565
  epc: https://www.erdosproblems.com/565
  author:
    informal:
      human:
        - Luís Aragão
        - Marcelo Campos
        - Gabriel Dahia
        - Rafael Filipe
        - João Pedro Marciano
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos565.md
  version: "4.33.0"

- key: ErdosProblems.Erdos570
  epc: https://www.erdosproblems.com/570
  author:
    informal:
      human:
        - Paul Erdős
        - Ralph Faudree
        - Cecil Rousseau
        - Richard Schelp
        - Wayne Goddard
        - Daniel Kleitman
        - Alexander Sidorenko
        - C. J. Jayawardene
        - Stijn Cambie
        - Alberto Freschi
        - Piotr Morawski
        - K. Petrova
        - Alexey Pokrovskiy
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos570.md
  version: "4.33.0"

- key: ErdosProblems.Erdos574
  epc: https://www.erdosproblems.com/574
  author:
    informal:
      human:
        - Felix Lazebnik
        - Vasiliy Ustimenko
        - Andrew Woldar
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos574.md
  version: "4.33.0"

- key: ErdosProblems.Erdos578
  epc: https://www.erdosproblems.com/578
  author:
    informal:
      human:
        - Oliver Riordan
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos578.md
  version: "4.33.0"

- key: ErdosProblems.Erdos581
  epc: https://www.erdosproblems.com/581
  author:
    informal:
      human:
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos581.md
  version: "4.33.0"

- key: ErdosProblems.Erdos582
  epc: https://www.erdosproblems.com/582
  author:
    informal:
      human: Jon Folkman
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/582
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos582.md
  version: "4.24.0"

- key: ErdosProblems.Erdos586
  epc: https://www.erdosproblems.com/586
  author:
    informal:
      human:
        - Paul Balister
        - Béla Bollobás
        - Robert Morris
        - Julian Sahasrabudhe
        - Marius Tiba
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos586.md
  version: "4.33.0"

- key: ErdosProblems.Erdos587
  epc: https://www.erdosproblems.com/587
  author:
    informal:
      human:
        - A. Khalfalah
        - S. Lodha
        - Endre Szemerédi
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos587.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/587.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos590
  epc: https://www.erdosproblems.com/590
  author:
    informal:
      human:
        - C. C. Chang
        - Jean A. Larson
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos590.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/590.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos593
  epc: https://www.erdosproblems.com/593
  author:
    informal:
      human:
        - Eric Li
        - Samuil Petkov
      AI:
        - GPT-5.5 Pro
        - GPT-5.6 Sol Pro
    formal:
      human: Samuil Petkov
      AI:
        - GPT-5.6 Pro
        - Aristotle
  arxiv: https://arxiv.org/abs/2606.24882
  url:
    - https://www.erdosproblems.com/forum/thread/593/proof-claims#proof-claim-54
    - https://github.com/SamPetkov/Erdos593/tree/bc763cdbe5a1cf971d9cc1c4cff92e41ebb69b3d/formalization
    - https://github.com/SamPetkov/Erdos593/blob/d834f1f42e7e0d5d2a6c23e9487563bedb1b277b/formalization/PROVENANCE.md
    - https://github.com/SamPetkov/Erdos593/blob/d834f1f42e7e0d5d2a6c23e9487563bedb1b277b/README.md
  version: "4.32.0"

- key: ErdosProblems.Erdos594
  epc: https://www.erdosproblems.com/594
  author:
    informal:
      human:
        - Paul Erdős
        - András Hajnal
        - Saharon Shelah
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos594.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/594.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos603
  epc: https://www.erdosproblems.com/603
  author:
    informal:
      human:
        - Przemek Chojecki
      AI:
        - GPT-5.4 Pro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos603.md
  version: "4.33.0"

- key: ErdosProblems.Erdos605
  epc: https://www.erdosproblems.com/605
  author:
    informal:
      human:
        - Paul Erdős
        - Dean Hickerson
        - János Pach
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos605.md
  version: "4.33.0"

- key: ErdosProblems.Erdos606
  epc: https://www.erdosproblems.com/606
  author:
    informal:
      human:
        - Paul Erdős
        - Peter Salamon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos606.md
  version: "4.33.0"

- key: ErdosProblems.Erdos607
  epc: https://www.erdosproblems.com/607
  author:
    informal:
      human:
        - Endre Szemerédi
        - William T. Trotter Jr.
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos607.md
  version: "4.33.0"

- key: ErdosProblems.Erdos608
  epc: https://www.erdosproblems.com/608
  author:
    informal:
      human:
        - Zoltán Füredi
        - Zeinab Maleki
    formal:
      AI: Claude Fable 5
      human: Emerson Hsieh
  url:
    - https://github.com/teorth/erdosproblems/pull/365
    - https://github.com/primateria/erdos608/tree/b50849234b8de6cb5c642b5cb0479cab2e9e9908
    - https://arxiv.org/abs/1605.09055
  version: "4.27.0"

- key: ErdosProblems.Erdos613
  epc: https://www.erdosproblems.com/613
  author:
    informal:
      human: Oleg Pikhurko
    formal:
      human: Terence Tao
  url:
    - https://www.erdosproblems.com/forum/thread/613#post-1678
    - https://github.com/teorth/analysis/blob/main/Analysis/Misc/erdos_613.lean
  version: "4.29.0-rc8"

- key: ErdosProblems.Erdos615
  epc: https://www.erdosproblems.com/615
  author:
    informal:
      human:
        - Jacob Fox
        - Po-Shen Loh
        - Yufei Zhao
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos615.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/615.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos618
  epc: https://www.erdosproblems.com/618
  author:
    informal:
      human: Noga Alon
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/618
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos618.md
  version: "4.24.0"

- key: ErdosProblems.Erdos619
  epc: https://www.erdosproblems.com/619
  author:
    informal:
      AI: Claude Fable 5
    formal:
      AI:
        - Claude Fable 5
        - GPT-5.5
        - Codex
      human: Nick Kuhn
  url:
    - https://www.erdosproblems.com/619#post-6986
    - https://github.com/nick-kuhn/erdos-619/tree/7f65718b8c1019ecc24e6c9a6b04ec4c66a4e26f
  version: "4.28.0"

- key: ErdosProblems.Erdos621
  epc: https://www.erdosproblems.com/621
  author:
    informal:
      human:
        - Sergey Norin
        - Yue Ru Sun
    formal:
      AI: Aristotle
      human: Lorenzo Luccioli
  url:
    - https://www.erdosproblems.com/forum/thread/621#post-5605
    - https://gist.githubusercontent.com/LorenzoLuccioli/71247a0c86fa35cb1e000160baef0bba/raw/eff1f49238af6ae9119b879ee91ff36ec6ee6b31/Erdos621.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos622
  epc: https://www.erdosproblems.com/622
  author:
    informal:
      human:
        - Nemanja Draganić
        - Peter Keevash
        - Alp Müyesser
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos622.md
  version: "4.33.0"

- key: ErdosProblems.Erdos630
  epc: https://www.erdosproblems.com/630
  author:
    informal:
      human:
        - Noga Alon
        - Michael Tarsi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos630.md
  version: "4.33.0"

- key: ErdosProblems.Erdos631
  epc: https://www.erdosproblems.com/631
  author:
    informal:
      human:
        - Carsten Thomassen
        - Margit Voigt
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos631.md
  version: "4.33.0"

- key: ErdosProblems.Erdos632
  epc: https://www.erdosproblems.com/632
  author:
    informal:
      human:
        - Zdeněk Dvořák
        - Xiaolan Hu
        - Jean-Sébastien Sereni
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos632.md
  version: "4.33.0"

- key: ErdosProblems.Erdos636
  epc: https://www.erdosproblems.com/636
  author:
    informal:
      human:
        - Matthew Kwan
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos636.md
  version: "4.33.0"

- key: ErdosProblems.Erdos637
  epc: https://www.erdosproblems.com/637
  author:
    informal:
      human:
        - Boris Bukh
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos637.md
  version: "4.33.0"

- key: ErdosProblems.Erdos639
  epc: https://www.erdosproblems.com/639
  author:
    informal:
      human:
        - Peter Keevash
        - Benny Sudakov
    formal:
      AI: Aristotle
      human: Jeremy Tan Jie Rui
  url:
    - https://www.erdosproblems.com/forum/thread/639#post-6189
    - https://gist.githubusercontent.com/Parcly-Taxel/f9a6a963d1057880633e4034294aa98e/raw/885ce8aa2d80d8ac598b98126de3321b5b8842ff/Erdos639.lean
    - https://gist.githubusercontent.com/Parcly-Taxel/f9a6a963d1057880633e4034294aa98e/raw/885ce8aa2d80d8ac598b98126de3321b5b8842ff/Erdos639.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos641
  epc: https://www.erdosproblems.com/641
  author:
    informal:
      human:
        - Barnabás Janzer
        - Richard Steiner
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos641.md
  version: "4.33.0"

- key: ErdosProblems.Erdos645
  epc: https://www.erdosproblems.com/645
  author:
    informal:
      human:
        - Tom C. Brown
        - Bruce M. Landman
        - Ryan Alweiss
      AI: ChatGPT 5.1 Pro
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/645
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos645.md
  version:
    - "4.20.0-rc5"
    - "4.24.0"

- key: ErdosProblems.Erdos646
  epc: https://www.erdosproblems.com/646
  author:
    informal:
      human: Daniel Berend
    formal:
      AI: Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/646#post-4507
  url_ref: JoshuaB_646
  version: "4.24.0"

- key: ErdosProblems.Erdos648
  epc: https://www.erdosproblems.com/648
  author:
    informal:
      human: Stijn Cambie
    formal:
      AI: Aristotle
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/2503.22691
  url:
    - https://www.erdosproblems.com/forum/thread/648
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos648.md
  version: "4.24.0"

- key: ErdosProblems.Erdos649
  epc: https://www.erdosproblems.com/649
  author:
    formal:
      AI:
        - ChatGPT
        - Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/649
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos649.md
  version: "4.24.0"

- key: ErdosProblems.Erdos650
  epc: https://www.erdosproblems.com/650
  author:
    informal:
      AI: GPT-5.4 Pro
      human:
        - Wouter van Doorn
        - Yixin He
        - Yanyang Li
        - Quanyu Tang
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/2603.28636
  url:
    - https://www.erdosproblems.com/forum/thread/650#post-4683
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem650.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos651
  epc: https://www.erdosproblems.com/651
  author:
    informal:
      human:
        - Cosmin Pohoata
        - Dmitrii Zakharov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos651.md
  version: "4.33.0"

- key: ErdosProblems.Erdos652
  epc: https://www.erdosproblems.com/652
  author:
    informal:
      human:
        - Surya Mathialagan
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos652.md
  version: "4.33.0"

- key: ErdosProblems.Erdos656
  epc: https://www.erdosproblems.com/656
  author:
    informal:
      human:
        - Bryna Kra
        - Joel Moreira
        - Florian K. Richter
        - Donald Robertson
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos656.md
  version: "4.33.0"

- key: ErdosProblems.Erdos658
  epc: https://www.erdosproblems.com/658
  author:
    informal:
      human:
        - József Solymosi
        - Peter Frankl
        - Vojtěch Rödl
    formal:
      AI: Aristotle
      human: John Jennings
  url:
    - https://www.erdosproblems.com/forum/thread/658#post-5654
    - https://www.erdosproblems.com/forum/thread/658#post-5677
    - https://gist.githubusercontent.com/JohnEdwardJennings/ca7d49761fb51d28613bafc956742fbc/raw/c326fd7918276292e641af92c32d3ecbe3c31ee0/Erdos658.lean
    - https://gist.githubusercontent.com/JohnEdwardJennings/ca7d49761fb51d28613bafc956742fbc/raw/93dbf493e26aa377f7e78390903be146745fa7ec/Erdos658.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos659
  epc: https://www.erdosproblems.com/659
  author:
    informal:
      human:
        - Benjamin Grayzel
        - Adam Sheffer
        - Pieter Moree
        - Robert Osburn
        - Desmond Weisenberg
      AI: Gemini
    statement: Formal Conjectures authors
    formal:
      AI:
        - Aristotle
        - Codex
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/math/0604163
  url:
    - https://www.erdosproblems.com/forum/thread/659
    - https://adamsheffer.wordpress.com/2014/07/16/point-sets-with-few-distinct-distances/
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos659.md
  version: "4.33.0"

- key: ErdosProblems.Erdos659b
  epc: https://www.erdosproblems.com/659
  author:
    informal:
      human:
        - Benjamin Grayzel
        - Adam Sheffer
        - Pieter Moree
        - Robert Osburn
        - Desmond Weisenberg
      AI: Gemini
    statement: Formal Conjectures authors
    formal:
      AI:
        - Aristotle
        - Codex
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/math/0604163
  url:
    - https://www.erdosproblems.com/forum/thread/659
    - https://adamsheffer.wordpress.com/2014/07/16/point-sets-with-few-distinct-distances/
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos659.md
  version: "4.33.0"

- key: ErdosProblems.Erdos664
  epc: https://www.erdosproblems.com/664
  author:
    informal:
      human:
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos664.md
  version: "4.33.0"

- key: ErdosProblems.Erdos666
  epc: https://www.erdosproblems.com/666
  author:
    informal:
      human:
        - Fan R. K. Chung
        - A. E. Brouwer
        - I. J. Dejter
        - Carsten Thomassen
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/666
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos666.md
  version: "4.24.0"

- key: ErdosProblems.Erdos671
  epc: https://www.erdosproblems.com/671
  author:
    informal:
      human:
        - Liam Price
        - QuietMethod
      AI:
        - GPT Pro
        - GPT-5.5
        - GPT-5 (Codex)
    formal:
      human:
        - Liam Price
        - QuietMethod
      AI:
        - GPT-5.5
        - GPT-5 (Codex)
  url:
    - https://www.erdosproblems.com/forum/thread/671/proof-claims#proof-claim-61
    - https://www.erdosproblems.com/forum/thread/671/proof-claims#proof-claim-127
    - https://quietmethod-erdos671.gintsuta-kobo.chatgpt.site/Erdos671_square_samples.lean
    - https://quietmethod-erdos671.gintsuta-kobo.chatgpt.site/
  version: "4.33.0-rc1"

- key: ErdosProblems.Erdos673
  epc: https://www.erdosproblems.com/673
  author:
    informal:
      human:
        - Paul Erdős
        - Gérald Tenenbaum
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos673.md
  version: "4.33.0"

- key: ErdosProblems.Erdos674
  epc: https://www.erdosproblems.com/674
  author:
    formal:
      human: Bhavik Mehta
  url: https://www.erdosproblems.com/forum/thread/674#post-2118
  url_ref: BhavikMehta_674
  version: "4.29.0"

- key: ErdosProblems.Erdos678
  epc: https://www.erdosproblems.com/678
  author:
    informal:
      human: Stijn Cambie
    formal:
      AI: Aristotle
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/2410.09138
  url:
    - https://www.erdosproblems.com/forum/thread/678
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos678.md
  version: "4.24.0"

- key: ErdosProblems.Erdos682
  epc: https://www.erdosproblems.com/682
  author:
    informal:
      human:
        - Ayla Gafni
        - Terence Tao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos682.md
  version: "4.33.0"

- key: ErdosProblems.Erdos690
  epc: https://www.erdosproblems.com/690
  author:
    informal:
      human:
        - Stijn Cambie
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos690.md
  version: "4.33.0"

- key: ErdosProblems.Erdos692
  epc: https://www.erdosproblems.com/692
  author:
    informal:
      human: Stijn Cambie
    formal:
      AI: Aristotle
      human: Pietro Monticone
  arxiv: https://arxiv.org/abs/2501.10333
  url:
    - https://www.erdosproblems.com/forum/thread/692#post-5204
    - https://gist.githubusercontent.com/pitmonticone/96516af9100a37a1da81908dc0b0410c/raw/a1d6ca7f3835c58b257e5e715c8fdf3a224e1bd0/Erdos692.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos694
  epc: https://www.erdosproblems.com/694
  author:
    informal:
      AI: GPT-5.5 Pro
      human: Liam Price
    formal:
      AI:
        - Claude Code 4.7
        - GPT-5.5 Pro
      human: Pawan Sasanka Ammanamanchi
  url:
    - https://www.erdosproblems.com/forum/thread/694#post-6202
    - https://www.overleaf.com/read/fgmhvywvdjkt#54ca5d
    - https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P694/Proof.lean
    - https://raw.githubusercontent.com/Shashi456/erdos-formalizations/refs/heads/main/Erdos/P694/Proof.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos697
  epc: https://www.erdosproblems.com/697
  author:
    informal:
      human:
        - Richard R. Hall
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos697.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/697.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos698
  epc: https://www.erdosproblems.com/698
  author:
    informal:
      human: George M. Bergman
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/698#post-3276
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem698.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos702
  epc: https://www.erdosproblems.com/702
  author:
    informal:
      human:
        - Péter Frankl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos702.md
  version: "4.33.0"

- key: ErdosProblems.Erdos703
  epc: https://www.erdosproblems.com/703
  author:
    informal:
      human:
        - Péter Frankl
        - Vojtěch Rödl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos703.md
  version: "4.33.0"

- key: ErdosProblems.Erdos705
  epc: https://www.erdosproblems.com/705
  author:
    informal:
      human:
        - Paul O'Donnell
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos705.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/705.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos707
  epc: https://www.erdosproblems.com/707
  author:
    informal:
      human:
        - Boris Alexeev
        - Dustin G. Mixon
      AI: ChatGPT
    formal:
      AI: ChatGPT
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/707
    - https://borisalexeev.com/papers/erdos707.html
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos707.md
  version: "4.24.0"

- key: ErdosProblems.Erdos715
  epc: https://www.erdosproblems.com/715
  author:
    informal:
      human:
        - V. A. Tashkinov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos715.md
  version: "4.33.0"

- key: ErdosProblems.Erdos716
  epc: https://www.erdosproblems.com/716
  author:
    informal:
      human:
        - Imre Z. Ruzsa
        - Endre Szemerédi
    formal:
      AI: Aristotle
      human: JoshuaB
  url:
    - https://www.erdosproblems.com/716#post-7096
    - https://aristotle.harmonic.fun/dashboard/requests/a876356c-15d8-4d24-b51f-001f57955616
  url_ref: JoshuaB_716
  version: "4.28.0"

- key: ErdosProblems.Erdos717
  epc: https://www.erdosproblems.com/717
  author:
    informal:
      human:
        - Jacob Fox
        - Choongbum Lee
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos717.md
  version: "4.33.0"

- key: ErdosProblems.Erdos718
  epc: https://www.erdosproblems.com/718
  author:
    informal:
      human:
        - János Komlós
        - Endre Szemerédi
        - Béla Bollobás
        - Andrew Thomason
        - Robin Thomas
        - Paul Wollan
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos718.md
  version: "4.33.0"

- key: ErdosProblems.Erdos720
  epc: https://www.erdosproblems.com/720
  author:
    informal:
      human:
        - József Beck
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos720.md
  version: "4.33.0"

- key: ErdosProblems.Erdos722
  epc: https://www.erdosproblems.com/722
  author:
    informal:
      human:
        - Peter Keevash
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos722.md
  version: "4.33.0"

- key: ErdosProblems.Erdos728
  epc: https://www.erdosproblems.com/728
  author:
    informal:
      AI: ChatGPT-5.2
      human: Kevin Barreto
    formal:
      AI: Aristotle
      human:
        - Kevin Barreto
        - Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/728#post-2828
    - https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos728b.lean
    - https://www.erdosproblems.com/forum/thread/728#post-2783
  version: "4.24.0"

- key: ErdosProblems.Erdos728p
  epc: https://www.erdosproblems.com/728
  author:
    informal:
      human: Carl Pomerance
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/728#post-3652
    - https://math.dartmouth.edu/~carlp/binom.pdf
    - https://raw.githubusercontent.com/plby/lean-proofs/refs/heads/main/src/v4.24.0/ErdosProblems/Erdos728p.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos729
  epc: https://www.erdosproblems.com/729
  author:
    informal:
      AI: GPT-5.2 Pro
      human:
        - Kevin Barreto
        - Liam Price
    formal:
      AI: Aristotle
      human: Kevin Barreto
  url: https://www.erdosproblems.com/forum/thread/729#post-2899
  version: "4.24.0"

- key: ErdosProblems.Erdos730
  epc: https://www.erdosproblems.com/730
  author:
    informal:
      human:
        - Liam Price
        - Tomodovodoo
        - Will Blair
      AI: GPT Pro
    formal:
      human: Will Blair
      AI:
        - Codex
        - Claude Code
  url:
    - https://www.erdosproblems.com/forum/thread/730/proof-claims#proof-claim-58
    - https://github.com/williamjblair/lean-proofs/tree/03729c9cbb0b602f5a828bb850c85e84c5a6d460/ErdosProblems/Erdos730
    - https://github.com/williamjblair/lean-proofs/tree/5d10b4d91f257cfbe8c563cf927f543a868845e0/ErdosProblems/Erdos730
    - https://palomar-registry.org/entry.html?id=PALOMAR-2026-08-22-000001&version=1
  version: 4.33.0
- key: ErdosProblems.Erdos732
  epc: https://www.erdosproblems.com/732
  author:
    informal:
      human:
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos732.md
  version: "4.33.0"

- key: ErdosProblems.Erdos733
  epc: https://www.erdosproblems.com/733
  author:
    informal:
      human:
        - Endre Szemerédi
        - William T. Trotter Jr.
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos733.md
  version: "4.33.0"

- key: ErdosProblems.Erdos735
  epc: https://www.erdosproblems.com/735
  author:
    informal:
      human:
        - Eyal Ackerman
        - Kevin Buchin
        - Christian Knauer
        - Rom Pinchasi
        - Günter Rote
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos735.md
  version: "4.33.0"

- key: ErdosProblems.Erdos737
  epc: https://www.erdosproblems.com/737
  author:
    informal:
      human:
        - Carsten Thomassen
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos737.md
  version: "4.33.0"

- key: ErdosProblems.Erdos741
  epc: https://www.erdosproblems.com/741
  author:
    informal:
      AI: a DeepMind prover agent
    formal:
      AI: a DeepMind prover agent
      human: Moritz Firsching
  url:
    - https://www.erdosproblems.com/forum/thread/741#post-5135
    - https://github.com/mo271/formal-conjectures/blob/486bc8afae062b6711cd16d3466d651ee2880a52/FormalConjectures/ErdosProblems/741.lean#L1449
    - https://github.com/mo271/formal-conjectures/blob/486bc8afae062b6711cd16d3466d651ee2880a52/FormalConjectures/ErdosProblems/741.lean#L1629
  version: "4.27.0"

- key: ErdosProblems.Erdos741b
  epc: https://www.erdosproblems.com/741
  author:
    informal:
      AI: GPT-5.4 Pro
      human: Przemek Chojecki
    formal:
      AI: Aristotle
      human: Przemek Chojecki
  url:
    - https://www.erdosproblems.com/forum/thread/741#post-5771
    - https://www.ulam.ai/research/erdos741.pdf
    - https://www.ulam.ai/research/erdos741.lean
  version: "4.29.1"

- key: ErdosProblems.Erdos742
  epc: https://www.erdosproblems.com/742
  author:
    informal:
      human:
        - Zoltán Füredi
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos742.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/742.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos744
  epc: https://www.erdosproblems.com/744
  author:
    informal:
      human:
        - Vojtěch Rödl
        - Zsolt Tuza
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos744.md
  version: "4.33.0"

- key: ErdosProblems.Erdos746
  epc: https://www.erdosproblems.com/746
  author:
    informal:
      human:
        - János Komlós
        - Endre Szemerédi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos746.md
  version: "4.33.0"

- key: ErdosProblems.Erdos748
  epc: https://www.erdosproblems.com/748
  author:
    informal:
      human:
        - Ben Green
        - Alexander Sapozhenko
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos748.md
  version: "4.33.0"

- key: ErdosProblems.Erdos751
  epc: https://www.erdosproblems.com/751
  author:
    informal:
      human:
        - J. A. Bondy
        - A. Vince
      AI: ChatGPT 5.2 Thinking
    formal:
      AI:
        - ChatGPT 5.2 Thinking
        - GPT-5.2 Codex
      human: scp020
  url:
    - https://www.erdosproblems.com/forum/thread/751#post-3835
    - https://people.clas.ufl.edu/avince/files/Cycles.pdf
    - https://github.com/SpringSense-Innovation-Institute/ai-for-math-lean/tree/main/erdos-problems/erdos751
  version: "4.23.0"

- key: ErdosProblems.Erdos752
  epc: https://www.erdosproblems.com/752
  author:
    informal:
      human:
        - Benny Sudakov
        - Jacques Verstraëte
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos752.md
  version: "4.33.0"

- key: ErdosProblems.Erdos753
  epc: https://www.erdosproblems.com/753
  author:
    informal:
      human: Noga Alon
    formal:
      AI: Aristotle
      human: Matteo Del Vecchio
  url:
    - https://www.erdosproblems.com/forum/thread/753#post-5373
    - https://gist.githubusercontent.com/madeve-unipi/80eaf8008c7c798b4f7b5baeb8c1812b/raw/70704b54755e9012597c99bab7db153786abfa8a/Erdos753.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos754
  epc: https://www.erdosproblems.com/754
  author:
    informal:
      human:
        - Konrad J. Swanepoel
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos754.md
  version: "4.33.0"

- key: ErdosProblems.Erdos755
  epc: https://www.erdosproblems.com/755
  author:
    informal:
      human:
        - Frank Clemen
        - Adrian Dumitrescu
        - Ding Liu
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos755.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/755.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos756
  epc: https://www.erdosproblems.com/756
  author:
    informal:
      human: K. Bhowmick
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/2407.01174
  url:
    - https://www.erdosproblems.com/forum/thread/756#post-4792
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem756.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos758
  epc: https://www.erdosproblems.com/758
  author:
    informal:
      human:
        - Bhavik Mehta
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos758.md
  version: "4.33.0"

- key: ErdosProblems.Erdos759
  epc: https://www.erdosproblems.com/759
  author:
    informal:
      human:
        - John Gimbel
        - Carsten Thomassen
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos759.md
  version: "4.33.0"

- key: ErdosProblems.Erdos760
  epc: https://www.erdosproblems.com/760
  author:
    informal:
      human:
        - Noga Alon
        - Michael Krivelevich
        - Benny Sudakov
    formal:
      AI: Aristotle
      human: Matteo Del Vecchio
  url:
    - https://www.erdosproblems.com/forum/thread/760#post-5727
    - https://gist.githubusercontent.com/madeve-unipi/a7ae50d445f95e73c360f442c3c84143/raw/e85a4b6a72e797488822bb5cbdfe68d9834e835c/Erdos760.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos762
  epc: https://www.erdosproblems.com/762
  author:
    informal:
      human: R. Steiner
    formal:
      AI:
        - Aristotle
        - ChatGPT
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/2408.02400
  url:
    - https://www.erdosproblems.com/forum/thread/762
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos762.md
  version: "4.24.0"

- key: ErdosProblems.Erdos763
  epc: https://www.erdosproblems.com/763
  author:
    informal:
      human:
        - Paul Erdős
        - W. H. J. Fuchs
        - Hugh Montgomery
        - Robert Vaughan
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos763.md
  version: "4.33.0"

- key: ErdosProblems.Erdos764
  epc: https://www.erdosproblems.com/764
  author:
    informal:
      human:
        - Robert Vaughan
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos764.md
  version: "4.33.0"

- key: ErdosProblems.Erdos765
  epc: https://www.erdosproblems.com/765
  author:
    informal:
      human:
        - István Reiman
        - Paul Erdős
        - Alfréd Rényi
        - W. G. Brown
    formal:
      AI: Aristotle
      human: Jeremy Tan Jie Rui
  url:
    - https://www.erdosproblems.com/765#post-6480
    - https://gist.githubusercontent.com/Parcly-Taxel/13d3bd0f1390b0832a42994a09cf91c5/raw/e267a3a494e64019a1a442b3b05438745923883b/Erdos765.lean
    - https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint/corollaries-chapter.html#prime_between
  version: "4.28.0"

- key: ErdosProblems.Erdos767
  epc: https://www.erdosproblems.com/767
  author:
    informal:
      human:
        - Tao Jiang
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos767.md
  version: "4.33.0"

- key: ErdosProblems.Erdos768
  epc: https://www.erdosproblems.com/768
  author:
    informal:
      human: Eric Li
      AI: GPT-5.5 Pro
    formal:
      human: Eric Li
      AI: Aristotle
  arxiv: https://arxiv.org/abs/2606.24872v2
  url:
    - https://www.erdosproblems.com/forum/thread/768/proof-claims#proof-claim-71
    - https://github.com/ericlisg/erdos768-lean/tree/v1.0.0
    - https://github.com/ericlisg/erdos768-lean/tree/e46ab245f1e5eb2d1f0b184874c4e32e02ad16c9
  version: 4.28.0
- key: ErdosProblems.Erdos771
  epc: https://www.erdosproblems.com/771
  author:
    informal:
      human:
        - Noga Alon
        - Gregory Freiman
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos771.md
  version: "4.33.0"

- key: ErdosProblems.Erdos772
  epc: https://www.erdosproblems.com/772
  author:
    informal:
      human:
        - Noga Alon
        - Paul Erdős
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos772.md
  version: "4.33.0"

- key: ErdosProblems.Erdos775
  epc: https://www.erdosproblems.com/775
  author:
    informal:
      human: Jun Gao
    formal:
      AI: Aristotle
      human: Lorenzo Luccioli
  url:
    - https://www.erdosproblems.com/forum/thread/775#post-5619
    - https://gist.githubusercontent.com/LorenzoLuccioli/dc7dac92dff47aac05b50f2562dbe8c1/raw/2c53e497b3d685bc4883c0a2394b5f10ecb367a0/Erdos775.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos777
  epc: https://www.erdosproblems.com/777
  author:
    informal:
      human:
        - Noga Alon
        - Péter Frankl
        - Shagnik Das
        - Roman Glebov
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos777.md
  version: "4.33.0"

- key: ErdosProblems.Erdos780
  epc: https://www.erdosproblems.com/780
  author:
    informal:
      human:
        - Noga Alon
        - Péter Frankl
        - László Lovász
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos780.md
  version: "4.33.0"

- key: ErdosProblems.Erdos781
  epc: https://www.erdosproblems.com/781
  author:
    informal:
      human:
        - Noga Alon
        - Joel Spencer
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos781.md
  version: "4.33.0"

- key: ErdosProblems.Erdos783
  epc: https://www.erdosproblems.com/783
  author:
    informal:
      human:
        - Terence Tao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos783.md
  version: "4.33.0"

- key: ErdosProblems.Erdos784
  epc: https://www.erdosproblems.com/784
  author:
    informal:
      human:
        - Imre Ruzsa
        - Andreas Weingartner
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos784.md
  version: "4.33.0"

- key: ErdosProblems.Erdos785
  epc: https://www.erdosproblems.com/785
  author:
    informal:
      human:
        - András Sárközy
        - Endre Szemerédi
        - Władysław Narkiewicz
        - Imre Z. Ruzsa
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/1510.00812
  url:
    - https://www.erdosproblems.com/forum/thread/785#post-4642
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem785.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos788
  epc: https://www.erdosproblems.com/788
  author:
    informal:
      human: Shouqiao Wang
      AI: GPT-5.6 Sol
    formal:
      human: Shouqiao Wang
  url:
    - https://www.erdosproblems.com/forum/thread/788/proof-claims#proof-claim-89
    - https://github.com/ShouqiaoW/erdos/tree/f2ae0edb45cbdb257e135d51ef855f64caeb348b/788/lean
  version: "4.27.0"

- key: ErdosProblems.Erdos793
  epc: https://www.erdosproblems.com/793
  author:
    informal:
      AI: GPT-5.6 Sol Ultra
      human: Przemek Chojecki
    formal:
      AI: Aristotle
      human:
        - Wouter van Doorn
        - Jake Mallen
  url:
    - https://www.erdosproblems.com/793#post-7596
    - https://github.com/Woett/Lean-files/blob/ce4bcdac98415c60c7a7d7f78ce54c9adb79bc47/ErdosProblem793.lean
    - https://github.com/Jayyhk/erdos-lean/tree/cc6c94bd3f9de7c4cf7703ed40d8fd06380780a3/problems/793
    - https://www.ulam.ai/research/erdos793.pdf
  version: "4.30.0"

- key: ErdosProblems.Erdos794
  epc: https://www.erdosproblems.com/794
  author:
    informal:
      human: Phillip Harris
    formal:
      AI:
        - Aristotle
        - ChatGPT
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/794
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos794.md
  version: "4.24.0"

- key: ErdosProblems.Erdos795
  epc: https://www.erdosproblems.com/795
  author:
    informal:
      human:
        - Paul Erdős
        - Rushil Raghavan
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos795.md
  version: "4.33.0"

- key: ErdosProblems.Erdos796
  epc: https://www.erdosproblems.com/796
  author:
    informal:
      human: Rishikesh Gajjala
      AI: GPT-5.6 Sol
    formal:
      human: Rishikesh Gajjala
      AI: GPT-5.6 Sol
  url:
    - https://www.erdosproblems.com/forum/thread/796/proof-claims#proof-claim-53
    - https://github.com/rishigajjala/erdos-796-lean/tree/37f72e245ffec2bc31326d2388547f05ab02f13c
    - https://github.com/rishigajjala/erdos-796-lean/blob/37f72e245ffec2bc31326d2388547f05ab02f13c/paper/On_Erdos_Multiplicative_Representation_Problem.pdf
  version: 4.30.0
- key: ErdosProblems.Erdos797
  epc: https://www.erdosproblems.com/797
  author:
    informal:
      human:
        - Noga Alon
        - Colin McDiarmid
        - Bruce Reed
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos797.md
  version: "4.33.0"

- key: ErdosProblems.Erdos798
  epc: https://www.erdosproblems.com/798
  author:
    informal:
      human: Noga Alon
    formal:
      AI: Aristotle
      human: Jeremy Tan Jie Rui
  url:
    - https://www.erdosproblems.com/forum/thread/798#post-6329
    - https://gist.githubusercontent.com/Parcly-Taxel/757ca8323d74784da1a776795b9c90a9/raw/3a9724b1f6cd2504b809cf3c66f843b89d375e8b/Erdos798.lean
    - https://gist.githubusercontent.com/Parcly-Taxel/757ca8323d74784da1a776795b9c90a9/raw/3a9724b1f6cd2504b809cf3c66f843b89d375e8b/Erdos798.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos799
  epc: https://www.erdosproblems.com/799
  author:
    informal:
      human:
        - Noga Alon
        - Michael Krivelevich
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos799.md
  version: "4.33.0"

- key: ErdosProblems.Erdos800
  epc: https://www.erdosproblems.com/800
  author:
    informal:
      human:
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos800.md
  version: "4.33.0"

- key: ErdosProblems.Erdos801
  epc: https://www.erdosproblems.com/801
  author:
    informal:
      human:
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos801.md
  version: "4.33.0"

- key: ErdosProblems.Erdos803
  epc: https://www.erdosproblems.com/803
  author:
    informal:
      human:
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos803.md
  version: "4.33.0"

- key: ErdosProblems.Erdos804
  epc: https://www.erdosproblems.com/804
  author:
    informal:
      human:
        - Noga Alon
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos804.md
  version: "4.33.0"

- key: ErdosProblems.Erdos806
  epc: https://www.erdosproblems.com/806
  author:
    informal:
      human:
        - Noga Alon
        - Boris Bukh
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos806.md
  version: "4.33.0"

- key: ErdosProblems.Erdos807
  epc: https://www.erdosproblems.com/807
  author:
    informal:
      human:
        - Noga Alon
        - Tom Bohman
        - Hao Huang
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos807.md
  version: "4.33.0"

- key: ErdosProblems.Erdos808
  epc: https://www.erdosproblems.com/808
  author:
    informal:
      human:
        - Noga Alon
        - Imre Ruzsa
        - József Solymosi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos808.md
  version: "4.33.0"

- key: ErdosProblems.Erdos814
  epc: https://www.erdosproblems.com/814
  author:
    informal:
      human:
        - Lisa Sauermann
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos814.md
  version: "4.33.0"

- key: ErdosProblems.Erdos815
  epc: https://www.erdosproblems.com/815
  author:
    informal:
      human:
        - Lothar Narins
        - Alexey Pokrovskiy
        - Tibor Szabó
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos815.md
  version: "4.33.0"

- key: ErdosProblems.Erdos816
  epc: https://www.erdosproblems.com/816
  author:
    informal:
      human:
        - Kaizhe Chen
        - Jie Ma
        - Zhen Liu
        - Qinghou Zeng
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos816.md
  version: "4.33.0"

- key: ErdosProblems.Erdos818
  epc: https://www.erdosproblems.com/818
  author:
    informal:
      human: József Solymosi
    formal:
      AI: Aristotle
      human: Tomaz Mascarenhas
  url:
    - https://www.erdosproblems.com/forum/thread/818#post-5890
    - https://gist.githubusercontent.com/tomaz1502/d8f3632157bae289e5d0ed68ccdc9433/raw/fa7570f83d63ead268ebe5478670f6c06142edcd/Erdos_818.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos823
  epc: https://www.erdosproblems.com/823
  author:
    informal:
      human:
        - Paul Pollack
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos823.md
  version: "4.33.0"

- key: ErdosProblems.Erdos825
  epc: https://www.erdosproblems.com/825
  author:
    informal:
      human:
        - Daniel Larsen
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos825.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/825.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos832
  epc: https://www.erdosproblems.com/832
  author:
    informal:
      human:
        - Noga Alon
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos832.md
  version: "4.33.0"

- key: ErdosProblems.Erdos833
  epc: https://www.erdosproblems.com/833
  author:
    informal:
      human:
        - Paul Erdős
        - László Lovász
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos833.md
  version: "4.33.0"

- key: ErdosProblems.Erdos834
  epc: https://www.erdosproblems.com/834
  author:
    informal:
      human:
        - R. Li
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos834.md
  version: "4.33.0"

- key: ErdosProblems.Erdos842
  epc: https://www.erdosproblems.com/842
  author:
    informal:
      human:
        - Herbert Fleischner
        - Michael Stiebitz
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos842.md
  version: "4.33.0"

- key: ErdosProblems.Erdos843
  epc: https://www.erdosproblems.com/843
  author:
    informal:
      human:
        - David Conlon
        - Jacob Fox
        - Huy Tuan Pham
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos843.md
  version: "4.33.0"

- key: ErdosProblems.Erdos844
  epc: https://www.erdosproblems.com/844
  author:
    informal:
      human:
        - Desmond Weisenberg
        - Václav Chvátal
    formal:
      AI: Aristotle
      human: John Jennings
  url:
    - https://www.erdosproblems.com/forum/thread/844#post-5919
    - https://users.encs.concordia.ca/~chvatal/conjecture.pdf
    - https://gist.githubusercontent.com/JohnEdwardJennings/e32f2c412b0225091e7519d60741bd2d/raw/7d811ea413e2f7c0c0442749958aaac421eb6807/Erdos844.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos845
  epc: https://www.erdosproblems.com/845
  author:
    informal:
      human:
        - Wouter van Doorn
        - Anneroos R. F. Everts
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/2511.04585
  url:
    - https://www.erdosproblems.com/forum/thread/845
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos845.md
  version: "4.24.0"

- key: ErdosProblems.Erdos846
  epc: https://www.erdosproblems.com/846
  author:
    informal:
      AI: a DeepMind prover agent
    statement: Formal Conjectures authors
    formal:
      AI: a DeepMind prover agent
      human: George Tsoukalas
  url:
    - https://www.erdosproblems.com/forum/thread/846#post-4447
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/846.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/2404258180688283e5141021c75464dc2acfb798/FormalConjectures/ErdosProblems/846.lean
  version: "4.22.0"

- key: ErdosProblems.Erdos847
  epc: https://www.erdosproblems.com/847
  author:
    informal:
      human:
        - Christian Reiher
        - Vojtěch Rödl
        - Marcelo Sales
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos847.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/847.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos848
  epc: https://www.erdosproblems.com/848
  author:
    informal:
      human:
        - Mehtaab Sawhney
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos848.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/848.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos851
  epc: https://www.erdosproblems.com/851
  author:
    informal:
      human:
        - Lisa Price
      AI:
        - GPT-5.2 Pro
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos851.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/851.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos858
  epc: https://www.erdosproblems.com/858
  author:
    informal:
      human:
        - Przemek Chojecki
      AI:
        - GPT-5.4 Pro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos858.md
  version: "4.33.0"

- key: ErdosProblems.Erdos861
  epc: https://www.erdosproblems.com/861
  author:
    informal:
      human:
        - David Saxton
        - Andrew Thomason
        - Yoshiharu Kohayakawa
        - Sang June Lee
        - Vojtěch Rödl
        - Wojciech Samotij
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos861.md
  version: "4.33.0"

- key: ErdosProblems.Erdos862
  epc: https://www.erdosproblems.com/862
  author:
    informal:
      human:
        - David Saxton
        - Andrew Thomason
      AI: ChatGPT
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human:
        - Boris Alexeev
        - Kevin Barreto
  url:
    - https://www.erdosproblems.com/forum/thread/862
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos862.md
  version: "4.24.0"

- key: ErdosProblems.Erdos863
  epc: https://www.erdosproblems.com/863
  author:
    informal:
      human:
        - Boon Suan Ho
        - Javier Cilleruelo
        - Imre Ruzsa
        - Carlos Trujillo
      AI:
        - GPT-5.4 Pro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos863.md
  version: "4.33.0"

- key: ErdosProblems.Erdos865
  epc: https://www.erdosproblems.com/865
  author:
    informal:
      AI: GPT-5.5 Pro
      human: Ricky Cipollini
    formal:
      AI: Aristotle
      human: Ricky Cipollini
  arxiv: https://arxiv.org/abs/2606.29361
  url:
    - https://www.erdosproblems.com/865#post-7378
    - https://github.com/mrricky22/erdos-865-lean/tree/54bfae36c1b0384737bc23b18180bdf001816c5d
  version: "4.28.0"

- key: ErdosProblems.Erdos866b
  partial: yes
  epc: https://www.erdosproblems.com/866
  author:
    informal:
      human: Wouter van Doorn
      AI: ChatGPT
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/2605.00040
  url:
    - https://www.erdosproblems.com/forum/thread/866#post-6229
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem866.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos867
  epc: https://www.erdosproblems.com/867
  author:
    informal:
      human: R. Freud
    formal:
      AI: Aristotle
      human: Pietro Monticone
  url:
    - https://www.erdosproblems.com/forum/thread/867#post-5279
    - https://gist.githubusercontent.com/pitmonticone/5c1b173e3140f869d7425d8f1003ac70/raw/2ae361451c92d1b033d144bc50212dc8e76abdc9/Erdos867.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos868
  epc: https://www.erdosproblems.com/868
  author:
    informal:
      human:
        - Daniel Larsen
        - Michael Larsen
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos868.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/868.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos869
  epc: https://www.erdosproblems.com/869
  author:
    informal:
      human:
        - Daniel Larsen
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos869.md
  version: "4.33.0"

- key: ErdosProblems.Erdos871
  epc: https://www.erdosproblems.com/871
  author:
    informal:
      human:
        - Paul Erdős
        - Melvyn B. Nathanson
        - Daniel Larsen
      AI: Claude Opus 4.5
    formal:
      AI:
        - Claude Opus 4.5
        - Gemini 3 Pro
      human:
        - Daniel Larsen
  url:
    - https://www.erdosproblems.com/forum/thread/871
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos871.md
  version: "4.24.0"

- key: ErdosProblems.Erdos874
  epc: https://www.erdosproblems.com/874
  author:
    informal:
      human:
        - Jean-Marc Deshouillers
        - Gregory Freiman
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos874.md
  version: "4.33.0"

- key: ErdosProblems.Erdos877
  epc: https://www.erdosproblems.com/877
  author:
    informal:
      human:
        - József Balogh
        - Hong Liu
        - Maryam Sharifzadeh
        - Andrew Treglown
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos877.md
  version: "4.33.0"

- key: ErdosProblems.Erdos880
  epc: https://www.erdosproblems.com/880
  author:
    informal:
      human:
        - Norbert Hegyvári
        - François Hennecart
        - Alain Plagne
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos880.md
  version: "4.33.0"

- key: ErdosProblems.Erdos882
  epc: https://www.erdosproblems.com/882
  author:
    informal:
      human:
        - Paul Erdős
        - Vsevolod F. Lev
        - Gérard Rauzy
        - Csaba Sándor
        - András Sárközy
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos882.md
  version: "4.33.0"

- key: ErdosProblems.Erdos884
  epc: https://www.erdosproblems.com/884
  author:
    informal:
      human:
        - Daniel Larsen
        - Terence Tao
    statement: Formal Conjectures authors
    formal:
      AI: Claude Fable 5
      human: R. J. Honicky
  url:
    - https://www.erdosproblems.com/884#post-7362
    - https://github.com/honicky/erdos884/tree/323e9a01306df1e094b434beaa48c018370fe258
    - https://github.com/Larsen-Daniel/Erdos-884/blob/main/884.pdf
    - https://terrytao.wordpress.com/wp-content/uploads/2025/09/erdos-884.pdf
  version: "4.31.0"

- key: ErdosProblems.Erdos888
  epc: https://www.erdosproblems.com/888
  author:
    informal:
      human:
        - Przemek Chojecki
      AI:
        - GPT-5.5 Pro
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos888.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/888.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos894
  epc: https://www.erdosproblems.com/894
  author:
    informal:
      human:
        - Yuval Peres
        - Wilhelm Schlag
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos894.md
  version: "4.33.0"

- key: ErdosProblems.Erdos895
  epc: https://www.erdosproblems.com/895
  author:
    informal:
      human:
        - Ben Barber
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos895.md
  version: "4.33.0"

- key: ErdosProblems.Erdos896
  epc: https://www.erdosproblems.com/896
  author:
    informal:
      human:
        - Przemek Chojecki
      AI:
        - GPT-5.5 Pro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos896.md
  version: "4.33.0"

- key: ErdosProblems.Erdos897
  epc: https://www.erdosproblems.com/897
  author:
    informal:
      human: Eduard Wirsing
      AI: Archivara Math Research Agent
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/897
    - https://archivara.org/paper/df04f023-6ef0-4c52-bd12-18cdaa8f0741
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos897.md
  version: "4.24.0"

- key: ErdosProblems.Erdos898
  epc: https://www.erdosproblems.com/898
  author:
    informal:
      human: Louis J. Mordell
      AI:
        - Gemini 3.0 Flash
        - Aristotle
    formal:
      AI:
        - Gemini 3.0 Flash
        - Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/898#post-3882
  url_ref: JoshuaB_898
  version: "4.24.0"

- key: ErdosProblems.Erdos899
  epc: https://www.erdosproblems.com/899
  author:
    informal:
      human:
        - Imre Ruzsa
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos899.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/899.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos900
  epc: https://www.erdosproblems.com/900
  author:
    informal:
      human:
        - Miklós Ajtai
        - János Komlós
        - Endre Szemerédi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos900.md
  version: "4.33.0"

- key: ErdosProblems.Erdos903
  epc: https://www.erdosproblems.com/903
  author:
    informal:
      human:
        - Paul Erdős
        - Joel Fowler
        - Vera T. Sós
        - Richard Wilson
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos903.md
  version: "4.33.0"

- key: ErdosProblems.Erdos904
  epc: https://www.erdosproblems.com/904
  author:
    informal:
      human:
        - Béla Bollobás
        - Vladimir Nikiforov
    formal:
      AI: Aristotle
      human: Jeremy Tan Jie Rui
  url:
    - https://www.erdosproblems.com/forum/thread/904#post-5573
    - https://gist.githubusercontent.com/Parcly-Taxel/876d4eadd49a0d29db91ed2e790db733/raw/f33e0451100317b6eda0dd48c971e8105ff8ea75/E904.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos905
  epc: https://www.erdosproblems.com/905
  author:
    informal:
      human:
        - N. G. Khadzhiivanov
        - S. V. Nikiforov
    formal:
      AI:
        - Aristotle
        - GPT 5.4
      human: Andres Gutierrez
  url: https://www.erdosproblems.com/forum/thread/905#post-5276
  version: "4.28.0"

- key: ErdosProblems.Erdos906
  epc: https://www.erdosproblems.com/906
  author:
    informal:
      human: Eric Hou
      AI: GPT-5.6 Sol
    formal:
      human: Eric Hou
      AI: GPT-5.6 Sol
  url:
    - https://www.erdosproblems.com/forum/thread/906/proof-claims#proof-claim-99
    - https://github.com/erichou1/cofinite-derivative-zeros/tree/d422aa284e6058721aeba9125b87bc658dbd52f5
    - https://github.com/erichou1/cofinite-derivative-zeros/tree/v1.0.0
    - https://github.com/erichou1/cofinite-derivative-zeros/blob/d422aa284e6058721aeba9125b87bc658dbd52f5/paper.tex
  version: "4.28.0"
- key: ErdosProblems.Erdos907
  epc: https://www.erdosproblems.com/907
  author:
    informal:
      human: N. G. de Bruijn
    formal:
      AI: Aristotle
      human: Pietro Monticone
  url:
    - https://www.erdosproblems.com/forum/thread/907#post-5277
    - https://gist.githubusercontent.com/pitmonticone/f419ac0a78259498f93fd60d49c0b3ea/raw/959cb0ef93596d9ade256e3cd0f4141e66176e04/Erdos907.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos908
  epc: https://www.erdosproblems.com/908
  author:
    informal:
      human:
        - Miklós Laczkovich
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos908.md
  version: "4.33.0"

- key: ErdosProblems.Erdos909
  epc: https://www.erdosproblems.com/909
  author:
    informal:
      human:
        - R. D. Anderson
        - J. E. Keisler
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos909.md
  version: "4.33.0"

- key: ErdosProblems.Erdos914
  epc: https://www.erdosproblems.com/914
  author:
    informal:
      human:
        - H. A. Kierstead
        - A. V. Kostochka
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/914#post-5403
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem914.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos915
  epc: https://www.erdosproblems.com/915
  author:
    informal:
      human:
        - Bo Sørensen
        - Carsten Thomassen
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos915.md
  version: "4.33.0"

- key: ErdosProblems.Erdos916
  epc: https://www.erdosproblems.com/916
  author:
    informal:
      human:
        - Carsten Thomassen
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos916.md
  version: "4.33.0"

- key: ErdosProblems.Erdos920
  epc: https://www.erdosproblems.com/920
  author:
    informal:
      human:
        - D. Bradač
        - Sam Mattheus
        - Jacques Verstraëte
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos920.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/920.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos921
  epc: https://www.erdosproblems.com/921
  author:
    informal:
      human:
        - H. A. Kierstead
        - Endre Szemerédi
        - William T. Trotter Jr.
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos921.md
  version: "4.33.0"

- key: ErdosProblems.Erdos922
  epc: https://www.erdosproblems.com/922
  author:
    informal:
      human:
        - Jon Folkman
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos922.md
  version: "4.33.0"

- key: ErdosProblems.Erdos923
  epc: https://www.erdosproblems.com/923
  author:
    informal:
      human: Vojtěch Rödl
    formal:
      AI: Aristotle
      human: Jeremy Tan Jie Rui
  url:
    - https://www.erdosproblems.com/forum/thread/923#post-5628
    - https://gist.githubusercontent.com/Parcly-Taxel/28b95db1e5d3e77077d30c07afc55992/raw/8069e58aa1abcbcff57e1c99addfbdeb8f32f302/E923-aristotle.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos924
  epc: https://www.erdosproblems.com/924
  author:
    informal:
      human:
        - Jaroslav Nešetřil
        - Vojtěch Rödl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos924.md
  version: "4.33.0"

- key: ErdosProblems.Erdos925
  epc: https://www.erdosproblems.com/925
  author:
    informal:
      human:
        - Noga Alon
        - Vojtěch Rödl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos925.md
  version: "4.33.0"

- key: ErdosProblems.Erdos926
  epc: https://www.erdosproblems.com/926
  author:
    informal:
      human:
        - Zoltán Füredi
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos926.md
  version: "4.33.0"

- key: ErdosProblems.Erdos927
  epc: https://www.erdosproblems.com/927
  author:
    informal:
      human: Joel H. Spencer
    formal:
      AI: Aristotle
      human:
        - John Jennings
        - Jake Mallen
  url:
    - https://www.erdosproblems.com/927#post-6850
    - https://gist.githubusercontent.com/JohnEdwardJennings/24c9debc9854cb118fbc1314c70941c3/raw/b4fc5ef91876a89018b10508c479c000258504fb/Erdos927.lean
    - https://github.com/Jayyhk/erdos-lean/tree/cc6c94bd3f9de7c4cf7703ed40d8fd06380780a3/problems/927
  version: "4.28.0"

- key: ErdosProblems.Erdos937
  epc: https://www.erdosproblems.com/937
  author:
    informal:
      human:
        - Prajeet Bajpai
        - Michael A. Bennett
        - Tsz Ho Chan
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos937.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/937.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos947
  epc: https://www.erdosproblems.com/947
  author:
    informal:
      AI: ChatGPT
      human: Wouter van Doorn
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/947#post-4068
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem947.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos948
  epc: https://www.erdosproblems.com/948
  author:
    informal:
      human:
        - Lisa Price
      AI:
        - GPT-5.5 Pro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos948.md
  version: "4.33.0"

- key: ErdosProblems.Erdos957
  epc: https://www.erdosproblems.com/957
  author:
    informal:
      human:
        - Adrian Dumitrescu
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos957.md
  version: "4.33.0"

- key: ErdosProblems.Erdos958
  epc: https://www.erdosproblems.com/958
  author:
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/958
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos958.md
  version: "4.24.0"

- key: ErdosProblems.Erdos960
  epc: https://www.erdosproblems.com/960
  author:
    informal:
      human:
        - Boris Alexeev
        - Matthew Putterman
        - Mehtaab Sawhney
        - Mark Sellke
        - Gregory Valiant
      AI:
        - OpenAI internal model
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos960.md
  version: "4.33.0"

- key: ErdosProblems.Erdos964
  epc: https://www.erdosproblems.com/964
  author:
    informal:
      human: Sean Eberhard
    formal:
      AI:
        - Aristotle
        - Gemini
        - Antigravity
      human: Daniel Chin
  arxiv: https://arxiv.org/abs/2505.00727
  url:
    - https://www.erdosproblems.com/forum/thread/964#post-4280
    - https://raw.githubusercontent.com/danielchin/proofs/refs/heads/main/Proofs/ErdosProblems/Erdos964.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos965
  epc: https://www.erdosproblems.com/965
  author:
    informal:
      human:
        - Péter Komjáth
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos965.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/965.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos966
  epc: https://www.erdosproblems.com/966
  author:
    informal:
      human: Joel Spencer
      AI: Aristotle
    formal:
      AI: Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/966#post-4472
  url_ref: JoshuaB_966
  version: "4.24.0"

- key: ErdosProblems.Erdos967
  epc: https://www.erdosproblems.com/967
  author:
    informal:
      human: Fredy Yip
    formal:
      AI: Aristotle
      human: Lawrence Wu
  arxiv: https://arxiv.org/abs/2512.16528
  url:
    - https://www.erdosproblems.com/forum/thread/967#post-2303
    - https://gist.githubusercontent.com/llllvvuu/d25f037d1f1000bdabd6ca928c74c9bb/raw/50871c3840af1e49c4e5acabefac6604c9b65c65/967.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos974
  epc: https://www.erdosproblems.com/974
  author:
    informal:
      human:
        - Robert Tijdeman
        - Quanyu Tang
    formal:
      AI: Aristotle
      human: Jeremy Tan Jie Rui
  url:
    - https://www.erdosproblems.com/forum/thread/974#post-5944
    - https://www.erdosproblems.com/forum/thread/974#post-640
    - https://gist.githubusercontent.com/Parcly-Taxel/a44cbf9a214a5358bf584d05265aec4c/raw/40bea6d343e4563e8f1c3d17b423deb72b3f8265/Erdos974.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos977
  epc: https://www.erdosproblems.com/977
  author:
    informal:
      human:
        - C. L. Stewart
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos977.md
  version: "4.33.0"

- key: ErdosProblems.Erdos980
  epc: https://www.erdosproblems.com/980
  author:
    informal:
      human:
        - P. D. T. A. Elliott
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos980.md
  version: "4.33.0"

- key: ErdosProblems.Erdos981
  epc: https://www.erdosproblems.com/981
  author:
    informal:
      human:
        - P. D. T. A. Elliott
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos981.md
  version: "4.33.0"

- key: ErdosProblems.Erdos984
  epc: https://www.erdosproblems.com/984
  author:
    informal:
      human:
        - Zach Hunter
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos984.md
  version: "4.33.0"

- key: ErdosProblems.Erdos986
  epc: https://www.erdosproblems.com/986
  author:
    informal:
      human:
        - D. Bradač
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos986.md
  version: "4.33.0"

- key: ErdosProblems.Erdos987
  epc: https://www.erdosproblems.com/987
  author:
    informal:
      human:
        - Boris Alexeev
        - Matthew Putterman
        - Mehtaab Sawhney
        - Mark Sellke
        - Gregory Valiant
      AI:
        - OpenAI internal model
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos987.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/987.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos988
  epc: https://www.erdosproblems.com/988
  author:
    informal:
      human:
        - Wolfgang M. Schmidt
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos988.md
  version: "4.33.0"

- key: ErdosProblems.Erdos990
  epc: https://www.erdosproblems.com/990
  author:
    informal:
      AI: an internal model at OpenAI
      human:
        - Boris Alexeev
        - Moe Putterman
        - Mehtaab Sawhney
        - Mark Sellke
        - Gregory Valiant
    formal:
      AI: Codex
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/2604.06609
  url: https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos990.md
  version: "4.29.0"

- key: ErdosProblems.Erdos990b
  epc: https://www.erdosproblems.com/990
  author:
    formal:
      AI: GPT-5.4 Pro
      human: Yuta Oriike
  url:
    - https://www.erdosproblems.com/forum/thread/990#post-5312
    - https://github.com/yuta0x89/ErdosProblems/blob/main/Erdos990.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos991
  epc: https://www.erdosproblems.com/991
  author:
    informal:
      human:
        - Jordi Marzo
        - Albert Mas
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos991.md
  version: "4.33.0"

- key: ErdosProblems.Erdos992
  epc: https://www.erdosproblems.com/992
  author:
    informal:
      human:
        - István Berkes
        - Walter Philipp
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos992.md
  version: "4.33.0"

- key: ErdosProblems.Erdos994
  epc: https://www.erdosproblems.com/994
  author:
    informal:
      human:
        - J. M. Marstrand
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos994.md
  version: "4.33.0"

- key: ErdosProblems.Erdos997
  epc: https://www.erdosproblems.com/997
  author:
    informal:
      AI: an internal model at OpenAI
      human:
        - Boris Alexeev
        - Moe Putterman
        - Mehtaab Sawhney
        - Mark Sellke
        - Gregory Valiant
    formal:
      AI: Aristotle
      human: Pietro Monticone
  arxiv: https://arxiv.org/abs/2603.29961
  url:
    - https://www.erdosproblems.com/forum/thread/997#post-5189
    - https://gist.githubusercontent.com/pitmonticone/016f2ed66b4cd1c4c4b9998095170e60/raw/b7dfc05c525ae385b5835f89f1ada721443e4305/Erdos997.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos998
  epc: https://www.erdosproblems.com/998
  author:
    informal:
      human:
        - Harry Kesten
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos998.md
  version: "4.33.0"

- key: ErdosProblems.Erdos999
  epc: https://www.erdosproblems.com/999
  author:
    informal:
      human:
        - Dimitris Koukoulopoulos
        - James Maynard
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos999.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1000
  epc: https://www.erdosproblems.com/1000
  author:
    informal:
      human: J. A. Haight
      AI: ChatGPT
    statement:
      AI: ChatGPT
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1000
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1000.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1001
  epc: https://www.erdosproblems.com/1001
  author:
    informal:
      human:
        - Harry Kesten
        - Vera T. Sós
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1001.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1002
  epc: https://www.erdosproblems.com/1002
  author:
    informal:
      human: Shouqiao Wang
      AI: GPT-5.6 Sol
    formal:
      human: Shouqiao Wang
  url:
    - https://www.erdosproblems.com/forum/thread/1002/proof-claims#proof-claim-106
    - https://github.com/ShouqiaoW/erdos/tree/a4ae3a7cf494331ab5b297c4680456c95aa38a3b/1002/lean
  version: "4.27.0"

- key: ErdosProblems.Erdos1005
  epc: https://www.erdosproblems.com/1005
  author:
    informal:
      human:
        - Ricky Cipollini
        - Wouter van Doorn
      AI:
        - GPT-5.5 Thinking
        - GPT-5.5 Pro
    formal:
      human:
        - Ricky Cipollini
        - Wouter van Doorn
      AI: Aristotle
  arxiv: https://arxiv.org/abs/2607.23302
  url:
    - https://www.erdosproblems.com/forum/thread/1005/proof-claims#proof-claim-9
    - https://github.com/Woett/Lean-files/blob/d30552f64c55686d40b928a0a3b8e2396357a4ee/ErdosProblem1005.lean
    - https://github.com/mrricky22/erdos-1005-lean/tree/b0b308115cd6502baae120c085b09861e45e7d1e
  version: "4.28.0"

- key: ErdosProblems.Erdos1006
  epc: https://www.erdosproblems.com/1006
  author:
    informal:
      human:
        - Jaroslav Nešetřil
        - Vojtěch Rödl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1006.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1007
  epc: https://www.erdosproblems.com/1007
  author:
    informal:
      human:
        - Roger F. House
        - Joe Chaffee
        - Matt Noble
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1007
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1007.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1008
  epc: https://www.erdosproblems.com/1008
  author:
    informal:
      human:
        - David Conlon
        - Jacob Fox
        - Benny Sudakov
        - Zach Hunter
      AI: ChatGPT
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/1401.6711
  url:
    - https://www.erdosproblems.com/forum/thread/1008
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1008.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1009
  epc: https://www.erdosproblems.com/1009
  author:
    informal:
      human:
        - E. Győri
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1009.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1012
  epc: https://www.erdosproblems.com/1012
  author:
    informal:
      human:
        - D. R. Woodall
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1012.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1014
  epc: https://www.erdosproblems.com/1014
  author:
    informal:
      AI: an internal model at OpenAI
    formal:
      AI: Codex
      human: Boris Alexeev
  url:
    - https://openai.com/index/introducing-gpt-5-5/
    - https://cdn.openai.com/pdf/6dc7175d-d9e7-4b8d-96b8-48fe5798cd5b/Ramsey.pdf
    - https://www.erdosproblems.com/forum/thread/1014#post-5749
  version: "4.29.0"

- key: ErdosProblems.Erdos1015
  epc: https://www.erdosproblems.com/1015
  author:
    informal:
      human:
        - S. A. Burr
        - Paul Erdős
        - Joel Spencer
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1015.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1018
  epc: https://www.erdosproblems.com/1018
  author:
    informal:
      human:
        - Alexandr Kostochka
        - László Pyber
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1018.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1019
  epc: https://www.erdosproblems.com/1019
  author:
    informal:
      human:
        - Miklós Simonovits
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1019.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1021
  epc: https://www.erdosproblems.com/1021
  author:
    informal:
      human:
        - Oliver Janzer
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1021.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1022
  epc: https://www.erdosproblems.com/1022
  author:
    informal:
      human: KoishiChan
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1022
    - https://www.erdosproblems.com/forum/thread/1022#post-2004
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1022.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1023
  epc: https://www.erdosproblems.com/1023
  author:
    informal:
      human:
        - Daniel Kleitman
        - Zach Hunter
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1023
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1023.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1024
  epc: https://www.erdosproblems.com/1024
  author:
    informal:
      human:
        - K. T. Phelps
        - Vojtěch Rödl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1024.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1025
  epc: https://www.erdosproblems.com/1025
  author:
    informal:
      human:
        - David Conlon
        - Jacob Fox
        - Benny Sudakov
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1025.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1026
  epc: https://www.erdosproblems.com/1026
  author:
    informal:
      human:
        - Desmond Weisenberg
        - Stijn Cambie
        - Wouter van Doorn
        - Thomas Bloom
        - Boris Alexeev
        - KoishiChan
        - Terence Tao
        - Lawrence Wu
        - Jineon Baek
        - Junnosuke Koizumi
        - Takahiro Ueoro
        - Iwan Praton
        - Adam Zsolt Wagner
        - J. Michael Steele
        - Abraham Seidenberg
      AI:
        - Aristotle
        - AlphaEvolve
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1026
    - https://terrytao.wordpress.com/2025/12/08/the-story-of-erdos-problem-126/
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1026.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1027
  epc: https://www.erdosproblems.com/1027
  author:
    informal:
      human:
        - Koishi Chan
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1027.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1028
  epc: https://www.erdosproblems.com/1028
  author:
    informal:
      human:
        - Paul Erdős
        - Joel Spencer
      AI: ChatGPT
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1028
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1028.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1031
  epc: https://www.erdosproblems.com/1031
  author:
    informal:
      human:
        - Hans Jürgen Prömel
        - Vojtěch Rödl
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1031.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1034
  epc: https://www.erdosproblems.com/1034
  author:
    informal:
      human:
        - Jie Ma
        - Quanyu Tang
      AI: ChatGPT
    statement:
      human: Boris Alexeev
    formal:
      AI: Aristotle
      human:
        - Namrata Anand
        - Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1034
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1034.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1036
  epc: https://www.erdosproblems.com/1036
  author:
    informal:
      human: Saharon Shelah
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1036
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1036.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1037
  epc: https://www.erdosproblems.com/1037
  author:
    informal:
      human:
        - Stijn Cambie
        - Zach Hunter
        - KoishiChan
    statement:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1037
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1037.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1038
  epc: https://www.erdosproblems.com/1038
  author:
    informal:
      human: Shouqiao Wang
      AI: GPT-5.6 Sol
    formal:
      AI: GPT
  url:
    - https://www.erdosproblems.com/forum/thread/1038/proof-claims#proof-claim-8
    - https://github.com/ShouqiaoW/erdos/tree/dc20752268ede5a3548e3d63ae74e45c3cfcf78c/1038/lean
  version: "4.27.0"

- key: ErdosProblems.Erdos1042
  epc: https://www.erdosproblems.com/1042
  author:
    informal:
      human:
        - Subhajit Ghosh
        - Koushik Ramachandran
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1042.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1043
  epc: https://www.erdosproblems.com/1043
  author:
    informal:
      human: Christian Pommerenke
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1043
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1043.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1044
  epc: https://www.erdosproblems.com/1044
  author:
    informal:
      human: Quanyu Tang
    formal:
      AI: Aristotle
      human: Lorenzo Luccioli
  url:
    - https://www.erdosproblems.com/forum/thread/1044#post-6012
    - https://github.com/QuanyuTang/erdos-problem-1044/blob/main/On_Erd%C5%91s_Problem_1044.pdf
    - https://gist.githubusercontent.com/LorenzoLuccioli/c3ace69881872112109a6c31b7a87cfc/raw
  version: "4.28.0"

- key: ErdosProblems.Erdos1046
  epc: https://www.erdosproblems.com/1046
  author:
    informal:
      human:
        - Christian Pommerenke
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1046.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1047
  epc: https://www.erdosproblems.com/1047
  author:
    informal:
      human:
        - Christian Pommerenke
        - A. W. Goodman
        - referee
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1047
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1047.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1048
  epc: https://www.erdosproblems.com/1048
  author:
    informal:
      human: Christian Pommerenke
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1048
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1048.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1048b
  epc: https://www.erdosproblems.com/1048
  author:
    informal:
      AI: Aristotle
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1048#post-3891
    - https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1048b.lean
    - https://raw.githubusercontent.com/plby/lean-proofs/refs/heads/main/src/v4.24.0/ErdosProblems/Erdos1048b.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos1050
  epc: https://www.erdosproblems.com/1050
  author:
    informal:
      human:
        - Peter B. Borwein
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1050.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1051
  epc: https://www.erdosproblems.com/1051
  author:
    informal:
      AI: Gemini Deep Think
      human:
        - Kevin Barreto
        - J. Kang
        - S. Kim
        - V. Kovac
        - S. Zhang
    formal:
      human: Kevin Barreto
  arxiv: https://arxiv.org/abs/2601.21442
  url:
    - https://www.erdosproblems.com/forum/thread/1051#post-3931
    - https://arxiv.org/abs/2601.21442
  version: "4.27.0"

- key: ErdosProblems.Erdos1056b
  partial: yes
  epc: https://www.erdosproblems.com/1056
  author:
    informal:
      AI: Aristotle
      human: Lorenzo Luccioli
    formal:
      AI: Aristotle
      human: Lorenzo Luccioli
  url:
    - https://www.erdosproblems.com/forum/thread/1056#post-2713
    - https://gist.githubusercontent.com/LorenzoLuccioli/62c1534cff0ae0268f4e5fb92f3f5ae2/raw/b5f2abd33e6a90bbd7693089f14babbddbefcdb7/1056_aristotle.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos1058
  epc: https://www.erdosproblems.com/1058
  author:
    informal:
      human:
        - Florian Luca
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1058.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1064
  epc: https://www.erdosproblems.com/1064
  author:
    informal:
      human:
        - Florian Luca
        - Carl Pomerance
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1064.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1064.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1067
  epc: https://www.erdosproblems.com/1067
  author:
    informal:
      human:
        - Péter Komjáth
        - Dániel T. Soukup
        - Nathan Bowler
        - Max Pitz
    statement:
      AI: ChatGPT
    formal:
      AI:
        - Aristotle
        - Aleph Prover
      human: Boris Alexeev
  arxiv: https://arxiv.org/abs/2402.05984
  url:
    - https://www.erdosproblems.com/forum/thread/1067
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1067.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1069
  epc: https://www.erdosproblems.com/1069
  author:
    informal:
      human:
        - Endre Szemerédi
        - William T. Trotter Jr.
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1069.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1071
  epc: https://www.erdosproblems.com/1071
  author:
    informal:
      human:
        - Everett Howe
        - Boris Alexeev
    formal:
      AI:
        - Aristotle
        - ChatGPT
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1071
    - https://www.erdosproblems.com/forum/thread/1071#post-4258
    - https://bsky.app/profile/ewhowe.com/post/3mbktyzvyak2e
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1071.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1076
  epc: https://www.erdosproblems.com/1076
  author:
    informal:
      human:
        - Stefan Glock
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1076.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1077
  epc: https://www.erdosproblems.com/1077
  author:
    informal:
      AI:
        - GPT-5.6 Sol
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1077.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1077.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1078
  epc: https://www.erdosproblems.com/1078
  author:
    informal:
      human:
        - Penny Haxell
        - Tibor Szabó
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1078.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1079
  epc: https://www.erdosproblems.com/1079
  author:
    informal:
      human:
        - Béla Bollobás
        - Andrew Thomason
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1079.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1080
  epc: https://www.erdosproblems.com/1080
  author:
    informal:
      human:
        - D. de Caen
        - L. A. Székely
      AI: ChatGPT
    statement: Formal Conjectures authors
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1080
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1080.md
  version: "4.24.0"

- key: ErdosProblems.Erdos1081
  epc: https://www.erdosproblems.com/1081
  author:
    informal:
      human:
        - Valentin Blomer
        - Andrew Granville
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1081.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1089
  epc: https://www.erdosproblems.com/1089
  author:
    informal:
      human:
        - Eiichi Bannai
        - Etsuko Bannai
        - Dennis Stanton
      AI:
        - Aletheia
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1089.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1090
  epc: https://www.erdosproblems.com/1090
  author:
    informal:
      human: Zach Hunter
    formal:
      AI:
        - Aristotle
        - Gemini 3.0 Flash
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/1090#post-4523
  url_ref: JoshuaB_1090
  version: "4.24.0"

- key: ErdosProblems.Erdos1092
  epc: https://www.erdosproblems.com/1092
  author:
    informal:
      human:
        - Vojtěch Rödl
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1092.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1092.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1095b
  partial: yes
  epc: https://www.erdosproblems.com/1095
  author:
    informal:
      human:
        - E. F. Ecklund Jr.
        - Paul Erdős
        - J. L. Selfridge
    statement:
      human:
        - Formal Conjectures authors
        - Boris Alexeev
    formal:
      AI: Aristotle
      human: Boris Alexeev
  url:
    - https://www.erdosproblems.com/forum/thread/1095#post-2605
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1095.md
    - https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1095b.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/3d6dc14ba924f82ab5200288f6c6ee1be1326a2d/FormalConjectures/ErdosProblems/1095.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos1096
  epc: https://www.erdosproblems.com/1096
  author:
    informal:
      human:
        - Paul Erdős
        - Vilmos Komornik
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1096.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1096.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1098
  epc: https://www.erdosproblems.com/1098
  author:
    informal:
      human: B. H. Neumann
    formal:
      AI: Aristotle
      human: John Jennings
  url:
    - https://www.erdosproblems.com/forum/thread/1098#post-5863
    - https://gist.githubusercontent.com/JohnEdwardJennings/783dce98df9fa6c333c24617ef07403b/raw/4963c590ee551175a3734014a8f08e8b86674e76/Erdos1098.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos1099
  epc: https://www.erdosproblems.com/1099
  author:
    informal:
      human:
        - Michael D. Vose
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1099.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1100b
  partial: yes
  conditional: PNT_statement
  epc: https://www.erdosproblems.com/1100
  author:
    informal:
      human:
        - Paul Erdős
        - R. R. Hall
        - Wouter van Doorn
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/1100#post-1659
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem1100.lean
  version: "4.24.0"

- key: ErdosProblems.Erdos1102
  epc: https://www.erdosproblems.com/1102
  author:
    informal:
      human:
        - Wouter van Doorn
        - Terence Tao
    formal:
      AI: Aristotle
      human: Wouter van Doorn
  arxiv: https://arxiv.org/abs/2512.01087
  url:
    - https://www.erdosproblems.com/forum/thread/1102#post-4415
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem1102PropertyP.lean
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem1102PropertyQDensity.lean
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem1102PropertyOverP.lean
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem1102PropertyQFastGrowing.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1102.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos1105
  epc: https://www.erdosproblems.com/1105
  author:
    informal:
      AI:
        - GPT-5.6 Sol
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1105.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1105.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1112
  epc: https://www.erdosproblems.com/1112
  author:
    informal:
      AI:
        - Claude Fable 5
        - Claude Opus 4.8
      human: Johan Land
    formal:
      AI:
        - Claude Fable 5
        - Claude Opus 4.8
      human: Johan Land
  url:
    - https://www.erdosproblems.com/1112#post-7375
    - https://github.com/beetree/math_erdos_1112/tree/63ed94d3e802782aeb521095c17d6109a2dc57b5
  version: "4.27.0"

- key: ErdosProblems.Erdos1114
  epc: https://www.erdosproblems.com/1114
  author:
    informal:
      human:
        - Elemér Bálint
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1114.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1115
  epc: https://www.erdosproblems.com/1115
  author:
    informal:
      human:
        - A. A. Gol'dberg
        - Alexandre Eremenko
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1115.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1116
  epc: https://www.erdosproblems.com/1116
  author:
    informal:
      human:
        - A. A. Gol'dberg
        - Sakari Toppila
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1116.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1118
  epc: https://www.erdosproblems.com/1118
  author:
    informal:
      human:
        - G. Camera
        - A. A. Gol'dberg
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1118.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1119
  epc: https://www.erdosproblems.com/1119
  author:
    informal:
      human:
        - Paul Erdős
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1119.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1119.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1121
  epc: https://www.erdosproblems.com/1121
  author:
    informal:
      human:
        - A. W. Goodman
        - R. E. Goodman
    formal:
      AI: Aristotle
      human: Amogh Parab
  url: https://www.erdosproblems.com/forum/thread/1121#post-5504
  version: "4.28.0"

- key: ErdosProblems.Erdos1124
  epc: https://www.erdosproblems.com/1124
  author:
    informal:
      human:
        - Miklós Laczkovich
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1124.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1125
  epc: https://www.erdosproblems.com/1125
  author:
    informal:
      human: Miklós Laczkovich
    formal:
      AI: Aristotle
      human: Stefano Rocca
  url:
    - https://www.erdosproblems.com/forum/thread/1125#post-5332
    - https://gist.githubusercontent.com/ster-oc/18384e6202ffe054cbc76ff2d0b1afde/raw/4d89f4dce1b6ae4aedde501bfbcbc4f9f81a8549/Erdos1125.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos1126
  epc: https://www.erdosproblems.com/1126
  author:
    informal:
      human: N. G. de Bruijn
    formal:
      AI: Aristotle
      human: JoshuaB
  url: https://www.erdosproblems.com/forum/thread/1126#post-4524
  url_ref: JoshuaB_1126
  version: "4.24.0"

- key: ErdosProblems.Erdos1127
  epc: https://www.erdosproblems.com/1127
  author:
    informal:
      human:
        - Kenneth Kunen
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1127.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1128
  epc: https://www.erdosproblems.com/1128
  author:
    informal:
      human:
        - Karel Prikry
        - George Mills
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1128.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1128.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1129
  epc: https://www.erdosproblems.com/1129
  author:
    informal:
      human:
        - Carl de Boor
        - Allan Pinkus
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1129.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1130
  epc: https://www.erdosproblems.com/1130
  author:
    informal:
      human:
        - Carl de Boor
        - Allan Pinkus
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1130.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1134
  epc: https://www.erdosproblems.com/1134
  author:
    informal:
      human:
        - D. J. Crampin
        - A. J. W. Hilton
    formal:
      AI: AxiomProver
  url:
    - https://www.erdosproblems.com/1134#post-7068
    - https://github.com/AxiomMath/erdos-public/blob/3ccf48c78b9df4aa26e1b2f90058bdd3f61da1ab/Erdos/Erdos1134/solution.lean
  version: "4.27.0"

- key: ErdosProblems.Erdos1136
  epc: https://www.erdosproblems.com/1136
  author:
    informal:
      human: Helmut Müller
    formal:
      AI: Aristotle
      human:
        - Lorenzo Luccioli
        - Wouter van Doorn
  url:
    - https://www.erdosproblems.com/forum/thread/1136#post-5688
    - https://github.com/Woett/Lean-files/blob/main/ErdosProblem1136.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos1138
  epc: https://www.erdosproblems.com/1138
  author:
    informal:
      human:
        - Hrishi Sunder
        - Sourish Kumrawat
        - Kireet Cheri
    formal:
      AI: Aristotle
      human: Lorenzo Luccioli
  url:
    - https://www.erdosproblems.com/forum/thread/1138#post-6243
    - https://gist.githubusercontent.com/LorenzoLuccioli/c7fbdd9809a616974b5587ee526c163b/raw
  version: "4.28.0"

- key: ErdosProblems.Erdos1140
  epc: https://www.erdosproblems.com/1140
  author:
    informal:
      human:
        - Mihai Epure
        - Alexandru Gica
        - Richard A. Mollin
        - Hugh C. Williams
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1140.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1141
  epc: https://www.erdosproblems.com/1141
  author:
    informal:
      AI: an internal model at OpenAI
      human:
        - Boris Alexeev
        - Moe Putterman
        - Mehtaab Sawhney
        - Mark Sellke
        - Gregory Valiant
    formal:
      AI: GPT-5.4 Pro
      human: Yuta Oriike
  arxiv: https://arxiv.org/abs/2604.06609
  url:
    - https://www.erdosproblems.com/forum/thread/1141#post-5335
    - https://github.com/yuta0x89/ErdosProblems/blob/a1319f732cdee5140faf47d984e2c451c1184803/Erdos1141.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1141.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1141b
  epc: https://www.erdosproblems.com/1141
  author:
    informal:
      AI: an internal model at OpenAI
      human:
        - Boris Alexeev
        - Moe Putterman
        - Mehtaab Sawhney
        - Mark Sellke
        - Gregory Valiant
    formal:
      AI: Codex
      human: Yuta Oriike
  arxiv: https://arxiv.org/abs/2604.06609
  url:
    - https://www.erdosproblems.com/forum/thread/1141#post-5335
    - https://github.com/yuta0x89/ErdosProblems/blob/a1319f732cdee5140faf47d984e2c451c1184803/Erdos1141.lean
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1141.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1147
  epc: https://www.erdosproblems.com/1147
  author:
    informal:
      human:
        - Jakub Konieczny
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1147.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1148
  epc: https://www.erdosproblems.com/1148
  author:
    informal:
      AI: GPT-5.4 Pro
      human: Przemek Chojecki
    formal:
      AI:
        - Gemini 3.1
        - Claude Opus 4.6
        - GPT-5.4 Pro
        - UlamAI Prover
      human: Przemek Chojecki
  url:
    - https://www.erdosproblems.com/forum/thread/1148#post-4849
    - https://www.ulam.ai/research/erdos1148-full.pdf
    - https://github.com/ulamai/ulamai
  url_ref: PrzemekChojecki_1148
  version: "4.27.0"

- key: ErdosProblems.Erdos1149
  epc: https://www.erdosproblems.com/1149
  author:
    informal:
      human:
        - Vitaly Bergelson
        - Florian Karl Richter
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1149.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1153
  epc: https://www.erdosproblems.com/1153
  author:
    informal:
      human:
        - Terence Tao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1153.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1161
  epc: https://www.erdosproblems.com/1161
  author:
    informal:
      human:
        - Adrian Beker
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1161.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1165
  epc: https://www.erdosproblems.com/1165
  author:
    informal:
      human:
        - C. Hao
        - X. Li
        - Izumi Okada
        - Y. Zheng
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1165.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1177
  epc: https://www.erdosproblems.com/1177
  author:
    informal:
      human: Eric Li
      AI: GPT-5.5 Pro
    formal:
      human: Eric Li
      AI: Aristotle
  arxiv: https://arxiv.org/abs/2606.24882v2
  url:
    - https://www.erdosproblems.com/forum/thread/1177/proof-claims#proof-claim-73
    - https://github.com/ericlisg/erdos-593-1177-lean/tree/v1.0.0
    - https://github.com/ericlisg/erdos-593-1177-lean/tree/5dcb6e4906df03f2e4294b21be73b55db7736f5a
  version: "4.28.0"

- key: ErdosProblems.Erdos1179
  epc: https://www.erdosproblems.com/1179
  author:
    informal:
      human:
        - Paul Erdős
        - Richard R. Hall
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1179.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1180
  epc: https://www.erdosproblems.com/1180
  author:
    informal:
      human:
        - A. A. Glibichuk
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1180.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1185
  epc: https://www.erdosproblems.com/1185
  author:
    informal:
      human:
        - Hillel Furstenberg
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1185.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1187
  epc: https://www.erdosproblems.com/1187
  author:
    informal:
      human:
        - Ben Green
        - Terence Tao
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1187.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1187b
  partial: yes
  epc: https://www.erdosproblems.com/1187
  author:
    formal:
      AI:
        - Codex
        - GPT-5.5 xhigh
      human: Kenta Kitamura
  url:
    - https://www.erdosproblems.com/forum/thread/1187#post-6429
    - https://github.com/KitaKen1/erdos-1187-lean
    - https://github.com/KitaKen1/erdos-1187-lean/blob/main/SecondSolution.lean
  version: "4.29.1"

- key: ErdosProblems.Erdos1188
  epc: https://www.erdosproblems.com/1188
  author:
    informal:
      human: Colin Snyder
      AI: GPT-5.6
    formal:
      human: Colin Snyder
      AI: GPT-5.6
  url:
    - https://www.erdosproblems.com/forum/thread/1188/proof-claims#proof-claim-51
    - https://www.starfleetmath.com/solutions/3ba934e6-6256-435e-bbd1-2a2ddc1ac5a7
    - https://www.starfleetmath.com/downloads/verify/erdos-1188/erdos-1188-solution.zip
  version: 4.31.0
- key: ErdosProblems.Erdos1190
  epc: https://www.erdosproblems.com/1190
  author:
    informal:
      AI: ChatGPT 5.5
      human: Malek Zribi
    formal:
      AI: Claude
      human: Pawan Sasanka Ammanamanchi
  url:
    - https://www.erdosproblems.com/forum/thread/1190#post-5988
    - https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P1190/Proof.lean
    - https://raw.githubusercontent.com/Shashi456/erdos-formalizations/refs/heads/main/Erdos/P1190/Proof.lean
  version: "4.27.0"

- key: ErdosProblems.Erdos1193
  epc: https://www.erdosproblems.com/1193
  author:
    formal:
      AI: Aristotle
      human: Pietro Monticone
  url:
    - https://www.erdosproblems.com/forum/thread/1193#post-5360
    - https://gist.githubusercontent.com/pitmonticone/c2658d464f8f5ca0e7fa40ed6fb78a5d/raw/793317d6a959dca24f5f313364c49c4c75fc5c01/Erdos1193.lean
  version: "4.28.0"

- key: ErdosProblems.Erdos1195
  epc: https://www.erdosproblems.com/1195
  author:
    informal:
      human:
        - Boon Suan Ho
      AI:
        - GPT-5.4 Pro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1195.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1196
  epc: https://www.erdosproblems.com/1196
  author:
    informal:
      AI: GPT-5.4 Pro
      human: Liam Price
    formal:
      AI: gauss-math-inc
      human: Math, Inc.
  url:
    - https://www.erdosproblems.com/forum/thread/1196#post-5469
    - https://github.com/math-inc/Erdos1196/tree/02fba13be7487cc51315f68d8fa7ef277633d3c8
    - https://github.com/math-inc/Erdos1196/blob/02fba13be7487cc51315f68d8fa7ef277633d3c8/PrimitiveSetsAboveX/FormalConjecturesErdos1196.lean
    - https://github.com/math-inc/Erdos1196/blob/02fba13be7487cc51315f68d8fa7ef277633d3c8/source.tex
  version: "4.30.0-rc1"

- key: ErdosProblems.Erdos1197
  epc: https://www.erdosproblems.com/1197
  author:
    informal:
      AI: GPT Pro
      human: Enrique Barschkis
    formal:
      AI:
        - Aristotle
        - GPT-5.4 Pro
      human:
        - Enrique Barschkis
        - Tom de Groot
  url:
    - https://www.erdosproblems.com/forum/thread/1197#post-5362
    - https://github.com/ebarschkis/ErdosProblem/blob/main/Problem1197/Solution.pdf
    - https://github.com/ebarschkis/ErdosProblem/blob/main/Problem1197/Solution.tex
    - https://github.com/ebarschkis/ErdosProblem/blob/main/Problem1197/Formalization.lean
    - https://github.com/Tomodovodoo/Erdos_1197
  version: "4.33.0"

- key: ErdosProblems.Erdos1198
  epc: https://www.erdosproblems.com/1198
  author:
    informal:
      human:
        - Gregory L. Smith
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1198.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1202
  epc: https://www.erdosproblems.com/1202
  author:
    informal:
      human:
        - Lisa Price
      AI:
        - GPT-5.4 Pro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1202.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1205
  epc: https://www.erdosproblems.com/1205
  author:
    informal:
      human:
        - Thomas Bloom
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1205.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1211
  epc: https://www.erdosproblems.com/1211
  author:
    informal:
      human:
        - David Conlon
        - Jacob Fox
        - Huy Tuan Pham
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1211.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1213
  epc: https://www.erdosproblems.com/1213
  author:
    informal:
      human:
        - Norbert Hegyvári
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1213.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1214
  epc: https://www.erdosproblems.com/1214
  author:
    informal:
      human:
        - Capi Corrales-Rodrigáñez
        - René Schoof
    statement: Formal Conjectures authors
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1214.md
    - https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1214.lean
  version: "4.33.0"

- key: ErdosProblems.Erdos1215
  epc: https://www.erdosproblems.com/1215
  author:
    informal:
      human:
        - Gerald R. Mac Lane
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1215.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1216
  epc: https://www.erdosproblems.com/1216
  author:
    informal:
      human:
        - K. B. Reid
        - E. T. Parker
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1216.md
  version: "4.33.0"

- key: ErdosProblems.Erdos1217
  epc: https://www.erdosproblems.com/1217
  author:
    informal:
      human:
        - Boris Alexeev
        - Kevin Barreto
        - Yuchen Li
        - Jared Duker Lichtman
        - Lisa Price
        - J. I. Shah
        - Q. Tang
        - Terence Tao
      AI:
        - GPT-5.4 Pro
    formal:
      AI:
        - Codex
        - GPT-5.6 Sol
  url:
    - https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos1217.md
  version: "4.33.0"