- number: "16"
  proof:
    path: "problems/16/"
    theorem: "Erdos16.erdos_16"
    state: "complete"
    last_update: "2026-05-23"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/16#post-4464"
      - "https://github.com/danielchin/proofs/blob/main/Proofs/ErdosProblems/Erdos16.lean"
- number: "24"
  proof:
    path: "problems/24/"
    theorem: "Erdos24.erdos_24"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/24#post-5732"
      - "https://gist.github.com/madeve-unipi/683739094ab7a5079a2bc2647c47743b#file-erdos24-lean"
- number: "26"
  proof:
    path: "problems/26/"
    theorem: "Erdos26.erdos_26"
    state: "complete"
    last_update: "2026-05-24"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/26#post-2532"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos26.lean"
- number: "31"
  proof:
    path: "problems/31/"
    theorem: "Erdos31.erdos_31"
    state: "complete"
    last_update: "2026-05-24"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/31#post-1818"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos31.lean"
- number: "34"
  proof:
    path: "problems/34/"
    theorem: "Erdos34.erdos_34"
    state: "complete"
    last_update: "2026-05-24"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/34#post-4197"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos34.lean"
- number: "38"
  proof:
    path: "problems/38/"
    theorem: "Erdos38.erdos_38"
    state: "complete"
    last_update: "2026-05-24"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/38#post-6131"
      - "https://gist.github.com/madeve-unipi/690d2bd8f6e8304ba8b456f9db559747#file-erdos38-lean"
- number: "42"
  proof:
    path: "problems/42/"
    theorem: "Erdos42.erdos_42"
    state: "complete"
    last_update: "2026-05-24"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/42#post-6370"
      - "https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P42/CompactCayley/Proof.lean"
- number: "45"
  proof:
    path: "problems/45/"
    theorem: "Erdos45.erdos_45"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.29.1"
    mathlib_revision: "5e932f97dd25535344f80f9dd8da3aab83df0fe6"
    sources:
      - "https://github.com/plby/unit-fractions/tree/master/src4"
- number: "46"
  proof:
    path: "problems/46/"
    theorem: "Erdos46.erdos_46"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.29.1"
    mathlib_revision: "5e932f97dd25535344f80f9dd8da3aab83df0fe6"
    sources:
      - "https://github.com/plby/unit-fractions/tree/master/src4"
- number: "47"
  proof:
    path: "problems/47/"
    theorem: "Erdos47.erdos_47"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.29.1"
    mathlib_revision: "5e932f97dd25535344f80f9dd8da3aab83df0fe6"
    sources:
      - "https://github.com/plby/unit-fractions/tree/master/src4"
- number: "56"
  proof:
    path: "problems/56/"
    theorem: "Erdos56.erdos_56"
    state: "complete"
    last_update: "2026-05-27"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/56#post-1850"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos56.lean"
- number: "71"
  proof:
    path: "problems/71/"
    theorem: "Erdos71.erdos_71"
    state: "complete"
    last_update: "2026-08-04"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/71#post-6635"
- number: "90"
  proof:
    path: "problems/90/"
    theorem: "Erdos90.erdos_90"
    state: "axiomatic"
    last_update: "2026-08-05"
    lean_toolchain: "leanprover/lean4:v4.29.1"
    mathlib_revision: "5e932f97dd25535344f80f9dd8da3aab83df0fe6"
    extra_axioms: ["Erdos90.golod_shafarevich_inequality", "Erdos90.shafarevich_relation_rank_bound"]
    sources:
      - "https://www.erdosproblems.com/forum/thread/90#post-6715"
      - "https://logicalintelligence.com/blog/aleph-prover-erdos-disproof-lean-4-formal-methods"
      - "https://github.com/logical-intelligence/erdos-unit-distance"
      - "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd"
- number: "93"
  proof:
    path: "problems/93/"
    theorem: "Erdos93.erdos_93"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/93#post-4346"
- number: "94"
  proof:
    path: "problems/94/"
    theorem: "Erdos94.erdos_94"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.21.0"
    mathlib_revision: "308445d7985027f538e281e18df29ca16ede2ba3"
    sources:
      - "https://www.erdosproblems.com/forum/thread/94"
      - "https://github.com/SpringSense-Innovation-Institute/ai-for-math-lean/blob/main/erdos-problems/erdos94/erdos94.lean"
- number: "105"
  proof:
    path: "problems/105/"
    theorem: "Erdos105.erdos_105"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/105#post-1746"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos105.lean"
- number: "115"
  proof:
    path: "problems/115/"
    theorem: "Erdos115.erdos_115"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/115#post-4555"
- number: "123"
  proof:
    path: "problems/123/"
    theorem: "Erdos123.erdos_123"
    state: "complete"
    last_update: "2026-07-22"
    lean_toolchain: "leanprover/lean4:v4.32.0"
    mathlib_revision: "81a5d257c8e410db227a6665ed08f64fea08e997"
    sources:
      - "https://www.erdosproblems.com/forum/thread/proof-claim:4c4dce98c5f14bb985b2c537e8fbf6ed#post-7652"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos123.lean"
- number: "125"
  proof:
    path: "problems/125/"
    theorem: "Erdos125.erdos_125"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/125#post-5110"
      - "https://github.com/mo271/formal-conjectures/blob/c27415379b5dbe34105d1fdd707994540c4c6fc7/FormalConjectures/ErdosProblems/125.lean#L468"
- number: "134"
  proof:
    path: "problems/134/"
    theorem: "Erdos134.erdos_134"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/134#post-4233"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos134.lean"
- number: "146"
  proof:
    path: "problems/146/"
    theorem: "Erdos146.erdos_146"
    state: "complete"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.32.0"
    mathlib_revision: "81a5d257c8e410db227a6665ed08f64fea08e997"
    sources:
      - "https://www.erdosproblems.com/forum/thread/146#post-8253"
      - "https://github.com/openai/ten-proofs/blob/main/CompactnessAndDegeneracy.lean"
- number: "150"
  proof:
    path: "problems/150/"
    theorem: "Erdos150.erdos_150"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/150#post-5145"
      - "https://gist.github.com/pitmonticone/d8558d3361ad2d673b5405239ea30700#file-erdos150-lean"
- number: "154"
  proof:
    path: "problems/154/"
    theorem: "Erdos154.erdos_154"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/154#post-4218"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem154.lean"
- number: "164"
  proof:
    path: "problems/164/"
    theorem: "Erdos164.erdos_164"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.29.0"
    mathlib_revision: "8a178386ffc0f5fef0b77738bb5449d50efeea95"
    sources:
      - "https://www.erdosproblems.com/forum/thread/164#post-5760"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.29.0/ErdosProblems/Erdos164.lean"
- number: "178"
  proof:
    path: "problems/178/"
    theorem: "Erdos178.erdos_178"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/178#post-5685"
      - "https://gist.github.com/madeve-unipi/ca9c3d1f94fe124c15726d836e1cd623#file-erdos178-lean"
- number: "180"
  proof:
    path: "problems/180/"
    theorem: "Erdos180.erdos_180"
    state: "complete"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.32.0"
    mathlib_revision: "81a5d257c8e410db227a6665ed08f64fea08e997"
    sources:
      - "https://www.erdosproblems.com/forum/thread/180#post-8255"
      - "https://github.com/openai/ten-proofs/blob/main/CompactnessAndDegeneracy.lean"
- number: "183"
  proof:
    path: "problems/183/"
    theorem: "Erdos183.erdos_183"
    state: "complete"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.32.0"
    mathlib_revision: "81a5d257c8e410db227a6665ed08f64fea08e997"
    sources:
      - "https://www.erdosproblems.com/forum/thread/183#post-8250"
      - "https://github.com/openai/ten-proofs/blob/main/MulticolorTriangleRamsey.lean"
- number: "189"
  proof:
    path: "problems/189/"
    theorem: "Erdos189.erdos_189"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/189#post-2281"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos189.lean"
- number: "192"
  proof:
    path: "problems/192/"
    theorem: "Erdos192.erdos_192"
    state: "complete"
    last_update: "2026-08-27"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/192#post-6375"
      - "https://gist.github.com/LorenzoLuccioli/f2ead0e5941e78a8fb78cf1d5925eca1#file-erdos192-lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos192.lean"
- number: "194"
  proof:
    path: "problems/194/"
    theorem: "Erdos194.erdos_194"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/194#post-5430"
      - "https://gist.github.com/ster-oc/ffe9e4fa1b813111f40c0e417bbe8be0#file-erdos194-lean"
- number: "198"
  proof:
    path: "problems/198/"
    theorem: "Erdos198.erdos_198"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/198#post-1809"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos198.lean"
- number: "199"
  proof:
    path: "problems/199/"
    theorem: "Erdos199.erdos_199"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/199#post-4442"
- number: "202"
  proof:
    path: "problems/202/"
    theorem: "Erdos202.erdos_202"
    state: "complete"
    last_update: "2026-05-31"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/202#post-6456"
      - "https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P202/Proof.lean"
- number: "204"
  proof:
    path: "problems/204/"
    theorem: "Erdos204.erdos_204"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/204#post-4790"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem204.lean"
- number: "205"
  proof:
    path: "problems/205/"
    theorem: "Erdos205.erdos_205"
    state: "complete"
    last_update: "2026-06-11"
    lean_toolchain: "leanprover/lean4:v4.30.0"
    mathlib_revision: "c5ea00351c28e24afc9f0f84379aa41082b1188f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/205"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos205.lean"
      - "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd"
- number: "206"
  proof:
    path: "problems/206/"
    theorem: "Erdos206.erdos_206"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/206#post-5989"
      - "https://gist.github.com/madeve-unipi/0920783513a1a00af4a14660852df60e#file-erdos206-lean"
- number: "209"
  proof:
    path: "problems/209/"
    theorem: "Erdos209.erdos_209"
    state: "complete"
    last_update: "2026-08-04"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/209#post-7065"
      - "https://github.com/AxiomMath/erdos-public/blob/main/Erdos/Erdos209/solution.lean"
- number: "214"
  proof:
    path: "problems/214/"
    theorem: "Erdos214.erdos_214"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/214#post-4547"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem214FourPoints.lean"
- number: "221"
  proof:
    path: "problems/221/"
    theorem: "Erdos221.erdos_221"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/221#post-3991"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem221.lean"
- number: "224"
  proof:
    path: "problems/224/"
    theorem: "Erdos224.erdos_224"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.25.0-rc2"
    mathlib_revision: "e93118937acf127bf5c203937d61eb25802c265a"
    sources:
      - "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"
- number: "226"
  proof:
    path: "problems/226/"
    theorem: "Erdos226.erdos_226"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/226#post-2574"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos226.lean"
- number: "229"
  proof:
    path: "problems/229/"
    theorem: "Erdos229.erdos_229"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/229#post-2514"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos229.lean"
- number: "231"
  proof:
    path: "problems/231/"
    theorem: "Erdos231.erdos_231"
    state: "complete"
    last_update: "2026-08-26"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/231#post-6376"
      - "https://gist.github.com/LorenzoLuccioli/d9854d75aa8494921cbb50c465a9b9dd#file-erdos231-lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos231.lean"
      - "https://github.com/AxiomMath/erdos-public/blob/main/Erdos/Erdos231/solution.lean"
- number: "237"
  proof:
    path: "problems/237/"
    theorem: "Erdos237.erdos_237"
    state: "complete"
    last_update: "2026-08-27"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/237#post-5240"
      - "https://gist.github.com/pitmonticone/8ea0d1cdb963b6213ac639b11d33f811#file-erdos237-lean"
      - "https://github.com/Woett/Lean-files/blob/main/MertensThird.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos237b.lean"
      - "https://github.com/frenzymath/FormalPantheon/tree/main/BoundedGaps"
- number: "246"
  proof:
    path: "problems/246/"
    theorem: "Erdos246.erdos_246"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/246#post-2513"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos246.lean"
- number: "258"
  proof:
    path: "problems/258/"
    theorem: "Erdos258.erdos_258"
    state: "complete"
    last_update: "2026-08-27"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/258#post-5682"
      - "https://gist.github.com/ster-oc/2b7adcf9d753cf6e29d782f7374cc57e#file-erdos258-lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos258b.lean"
      - "https://github.com/frenzymath/FormalPantheon/tree/main/BoundedGaps"
- number: "259"
  proof:
    path: "problems/259/"
    theorem: "Erdos259.erdos_259"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/259#post-5683"
      - "https://gist.github.com/ster-oc/c7429943f6b3a634797dc8b2a3b01f2d#file-erdos259-lean"
- number: "268"
  proof:
    path: "problems/268/"
    theorem: "Erdos268.erdos_268"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/268#post-5359"
      - "https://gist.github.com/madeve-unipi/62a8f68cdb4864b85b81a6752dcb0aa4#file-erdos268-lean"
- number: "275"
  proof:
    path: "problems/275/"
    theorem: "Erdos275.erdos_275"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/275#post-3543"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos275.lean"
- number: "280"
  proof:
    path: "problems/280/"
    theorem: "Erdos280.erdos_280"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/280#post-5595"
      - "https://gist.github.com/LorenzoLuccioli/2dda92a192c15c24263c8a258979e7e3#file-erdos280-lean"
- number: "281"
  proof:
    path: "problems/281/"
    theorem: "Erdos281.erdos_281"
    state: "complete"
    last_update: "2026-05-23"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/281#post-3445"
- number: "283"
  proof:
    path: "problems/283/"
    theorem: "Erdos283.erdos_283"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/283#post-6290"
      - "https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P283/Proof_flat.lean"
- number: "290"
  proof:
    path: "problems/290/"
    theorem: "Erdos290.erdos_290"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/290#post-3180"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem290.lean"
- number: "296"
  proof:
    path: "problems/296/"
    theorem: "Erdos296.erdos_296"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.29.1"
    mathlib_revision: "5e932f97dd25535344f80f9dd8da3aab83df0fe6"
    sources:
      - "https://www.erdosproblems.com/forum/thread/296#post-5713"
      - "https://gist.github.com/JohnEdwardJennings/d1ba8d7b8c63cc7eade1243e19e2eb35#file-erdos296-lean"
      - "https://github.com/plby/unit-fractions/tree/master/src4"
- number: "298"
  proof:
    path: "problems/298/"
    theorem: "Erdos298.erdos_298"
    state: "complete"
    last_update: "2026-05-25"
    lean_toolchain: "leanprover/lean4:v4.29.1"
    mathlib_revision: "5e932f97dd25535344f80f9dd8da3aab83df0fe6"
    sources:
      - "https://github.com/plby/unit-fractions/tree/master/src4"
- number: "299"
  proof:
    path: "problems/299/"
    theorem: "Erdos299.erdos_299"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.29.1"
    mathlib_revision: "5e932f97dd25535344f80f9dd8da3aab83df0fe6"
    sources:
      - "https://github.com/plby/unit-fractions/blob/master/src4/ErdosProblems.lean"
- number: "303"
  proof:
    path: "problems/303/"
    theorem: "Erdos303.erdos_303"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.22.0"
    mathlib_revision: "79e94a093aff4a60fb1b1f92d9681e407124c2ca"
    sources:
      - "https://www.erdosproblems.com/forum/thread/303#post-2347"
- number: "314"
  proof:
    path: "problems/314/"
    theorem: "Erdos314.erdos_314"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/314#post-5193"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem314.lean"
- number: "315"
  proof:
    path: "problems/315/"
    theorem: "Erdos315.erdos_315"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/315#post-4020"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos315.lean"
- number: "316"
  proof:
    path: "problems/316/"
    theorem: "Erdos316.erdos_316"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/316.lean"
- number: "328"
  proof:
    path: "problems/328/"
    theorem: "Erdos328.erdos_328"
    state: "complete"
    last_update: "2026-06-21"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/328#post-7066"
      - "https://github.com/AxiomMath/erdos-public/blob/main/Erdos/Erdos328/solution.lean"
- number: "330"
  proof:
    path: "problems/330/"
    theorem: "Erdos330.erdos_330"
    state: "complete"
    last_update: "2026-08-06"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/330#post-6271"
      - "https://github.com/AllenGrahamHart/FormalConjectures-Bench/tree/main/formalizations/erdos330"
- number: "331"
  proof:
    path: "problems/331/"
    theorem: "Erdos331.erdos_331"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/331#post-4019"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem331.lean"
- number: "333"
  proof:
    path: "problems/333/"
    theorem: "Erdos333.erdos_333"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/333#post-2403"
- number: "337"
  proof:
    path: "problems/337/"
    theorem: "Erdos337.erdos_337"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/337#post-2142"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos337.lean"
- number: "347"
  proof:
    path: "problems/347/"
    theorem: "Erdos347.erdos_347"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/347#post-3610"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem347.lean"
- number: "350"
  proof:
    path: "problems/350/"
    theorem: "Erdos350.erdos_350"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/350#post-1848"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos350.lean"
- number: "351"
  proof:
    path: "problems/351/"
    theorem: "Erdos351.erdos_351"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/283#post-6290"
      - "https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P283/Proof_flat.lean"
- number: "353"
  proof:
    path: "problems/353/"
    theorem: "Erdos353.erdos_353"
    state: "complete"
    last_update: "2026-08-04"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/353#post-7085"
      - "https://aristotle.harmonic.fun/dashboard/requests/75cddfef-5f21-4eef-8490-7ed7d1163368"
      - "https://www.erdosproblems.com/forum/thread/353#post-7095"
      - "https://aristotle.harmonic.fun/dashboard/requests/c4fea4e2-cb48-4377-beea-4d91133951ca"
      - "https://www.erdosproblems.com/forum/thread/353#post-7098"
      - "https://aristotle.harmonic.fun/dashboard/requests/f90b7996-0e71-4e59-87d2-03504f3d6c45"
- number: "355"
  proof:
    path: "problems/355/"
    theorem: "Erdos355.erdos_355"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/355#post-4741"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem355.lean"
- number: "363"
  proof:
    path: "problems/363/"
    theorem: "Erdos363.erdos_363"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/363#post-4709"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem363.lean"
- number: "369"
  proof:
    path: "problems/369/"
    theorem: "Erdos369.erdos_369"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/369#post-5058"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem369.lean"
- number: "370"
  proof:
    path: "problems/370/"
    theorem: "Erdos370.erdos_370"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/370#post-1813"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos370.lean"
- number: "379"
  proof:
    path: "problems/379/"
    theorem: "Erdos379.erdos_379"
    state: "complete"
    last_update: "2026-05-26"
    lean_toolchain: "leanprover/lean4:v4.22.0"
    mathlib_revision: "79e94a093aff4a60fb1b1f92d9681e407124c2ca"
    sources:
      - "https://www.erdosproblems.com/forum/thread/379#post-2350"
- number: "392"
  proof:
    path: "problems/392/"
    theorem: "Erdos392.erdos_392"
    state: "complete"
    last_update: "2026-06-05"
    lean_toolchain: "leanprover/lean4:v4.29.0"
    mathlib_revision: "8a178386ffc0f5fef0b77738bb5449d50efeea95"
    sources:
      - "https://www.erdosproblems.com/forum/thread/392#post-4410"
      - "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/Erdos392.lean"
- number: "397"
  proof:
    path: "problems/397/"
    theorem: "Erdos397.erdos_397"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/397#post-2940"
      - "https://gist.github.com/llllvvuu/40d68cfa9de9f43eece07ff4fdc3b0ef#file-397-lean"
- number: "399"
  proof:
    path: "problems/399/"
    theorem: "Erdos399.erdos_399"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/399.lean"
- number: "401"
  proof:
    path: "problems/401/"
    theorem: "Erdos401.erdos_401"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/401#post-3002"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos401b.lean"
- number: "403"
  proof:
    path: "problems/403/"
    theorem: "Erdos403.erdos_403"
    state: "complete"
    last_update: "2026-06-21"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/403#post-7067"
      - "https://github.com/AxiomMath/erdos-public/blob/main/Erdos/Erdos403/solution.lean"
- number: "418"
  proof:
    path: "problems/418/"
    theorem: "Erdos418.erdos_418"
    state: "complete"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.32.0"
    mathlib_revision: "81a5d257c8e410db227a6665ed08f64fea08e997"
    sources:
      - "https://www.erdosproblems.com/forum/thread/418#post-1778"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.32.0/ErdosProblems/Erdos418.lean"
- number: "419"
  proof:
    path: "problems/419/"
    theorem: "Erdos419.erdos_419"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/419#post-3992"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos419.lean"
- number: "426"
  proof:
    path: "problems/426/"
    theorem: "Erdos426.erdos_426"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/426#post-5775"
      - "https://gist.github.com/LorenzoLuccioli/6740274ef8c8bd77a6c966887a72b198#file-erdos426-lean"
- number: "427"
  proof:
    path: "problems/427/"
    theorem: "Erdos427.erdos_427"
    state: "axiomatic"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    extra_axioms: ["Erdos427.shiu_consecutive_primes"]
    sources:
      - "https://www.erdosproblems.com/forum/thread/427#post-5920"
      - "https://gist.github.com/JohnEdwardJennings/e2c6ef0daab55857b7cc9d340de7af84#file-erdos427-lean"
- number: "429"
  proof:
    path: "problems/429/"
    theorem: "Erdos429.erdos_429"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/429#post-3910"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem429.lean"
- number: "433"
  proof:
    path: "problems/433/"
    theorem: "Erdos433.erdos_433"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.29.0"
    mathlib_revision: "8a178386ffc0f5fef0b77738bb5449d50efeea95"
    sources:
      - "https://www.erdosproblems.com/forum/thread/433#post-4436"
      - "https://github.com/YaelDillies/MiscYD/blob/master/MiscYD/AddCombi/Kneser/Kneser.lean"
- number: "434"
  proof:
    path: "problems/434/"
    theorem: "Erdos434.erdos_434"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.29.0"
    mathlib_revision: "8a178386ffc0f5fef0b77738bb5449d50efeea95"
    sources:
      - "https://www.erdosproblems.com/forum/thread/434#post-4437"
      - "https://github.com/YaelDillies/MiscYD/blob/master/MiscYD/AddCombi/Kneser/Kneser.lean"
- number: "435"
  proof:
    path: "problems/435/"
    theorem: "Erdos435.erdos_435"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/435#post-4173"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos435.lean"
- number: "443"
  proof:
    path: "problems/443/"
    theorem: "Erdos443.erdos_443"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/443#post-4149"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos443.lean"
- number: "447"
  proof:
    path: "problems/447/"
    theorem: "Erdos447.erdos_447"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/447#post-4248"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos447.lean"
- number: "453"
  proof:
    path: "problems/453/"
    theorem: "Erdos453.erdos_453"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/453#post-4022"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos453.lean"
- number: "457"
  proof:
    path: "problems/457/"
    theorem: "Erdos457.erdos_457"
    state: "complete"
    last_update: "2026-05-28"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/457#post-4668"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem457.lean"
- number: "459"
  proof:
    path: "problems/459/"
    theorem: "Erdos459.erdos_459"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/459#post-4716"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem459.lean"
- number: "464"
  proof:
    path: "problems/464/"
    theorem: "Erdos464.erdos_464"
    state: "complete"
    last_update: "2026-08-04"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/464#post-7120"
      - "https://aristotle.harmonic.fun/dashboard/requests/f9894d2d-4bb1-42da-9301-e508aa881b17"
- number: "469"
  proof:
    path: "problems/469/"
    theorem: "Erdos469.erdos_469"
    state: "complete"
    last_update: "2026-07-23"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/proof-claim:c41518b56dd744eda333dc3c1f694516#post-7583"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem469.lean"
- number: "476"
  proof:
    path: "problems/476/"
    theorem: "Erdos476.erdos_476"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/476#post-2614"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos476.lean"
- number: "481"
  proof:
    path: "problems/481/"
    theorem: "Erdos481.erdos_481"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/481#post-1930"
- number: "484"
  proof:
    path: "problems/484/"
    theorem: "Erdos484.erdos_484"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/484#post-5448"
- number: "487"
  proof:
    path: "problems/487/"
    theorem: "Erdos487.erdos_487"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/487#post-4327"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos487.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos447.lean"
- number: "490"
  proof:
    path: "problems/490/"
    theorem: "Erdos490.erdos_490"
    state: "complete"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/490#post-6497"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem490.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos490.lean"
- number: "493"
  proof:
    path: "problems/493/"
    theorem: "Erdos493.erdos_493"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/493#post-2456"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos493.lean"
- number: "497"
  proof:
    path: "problems/497/"
    theorem: "Erdos497.erdos_497"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/497#post-4154"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos497.lean"
- number: "498"
  proof:
    path: "problems/498/"
    theorem: "Erdos498.erdos_498"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/498#post-3844"
- number: "499"
  proof:
    path: "problems/499/"
    theorem: "Erdos499.erdos_499"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/499#post-1889"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos499.lean"
- number: "502"
  proof:
    path: "problems/502/"
    theorem: "Erdos502.erdos_502"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/502#post-4106"
- number: "505"
  proof:
    path: "problems/505/"
    theorem: "Erdos505.erdos_505"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/505#post-4108"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos505.lean"
- number: "512"
  proof:
    path: "problems/512/"
    theorem: "Erdos512.erdos_512"
    state: "complete"
    last_update: "2026-06-22"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/512#post-7140"
      - "https://aristotle.harmonic.fun/dashboard/requests/b663fac0-b653-4148-8d0a-9ae5c7dbdaea"
- number: "519"
  proof:
    path: "problems/519/"
    theorem: "Erdos519.erdos_519"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/519#post-5599"
      - "https://gist.github.com/JohnEdwardJennings/db1e0cb00b7d6866193c12f1c70a1813#file-erdos519-lean"
- number: "532"
  proof:
    path: "problems/532/"
    theorem: "Erdos532.erdos_532"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/532#post-4004"
      - "https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Hindman.html"
- number: "537"
  proof:
    path: "problems/537/"
    theorem: "Erdos537.erdos_537"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/537#post-4225"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos537.lean"
- number: "540"
  proof:
    path: "problems/540/"
    theorem: "Erdos540.erdos_540"
    state: "complete"
    last_update: "2026-05-29"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/540#post-5410"
      - "https://gist.github.com/madeve-unipi/e5b448ddfb84f4c5427d22555f19b1e6#file-erdos540-lean"
- number: "541"
  proof:
    path: "problems/541/"
    theorem: "Erdos541.erdos_541"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/541#post-2617"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos541.lean"
- number: "582"
  proof:
    path: "problems/582/"
    theorem: "Erdos582.erdos_582"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/582#post-4212"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos582.lean"
- number: "608"
  proof:
    path: "problems/608/"
    theorem: "Erdos608.erdos_608"
    state: "complete"
    last_update: "2026-08-05"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://github.com/primateria/erdos608"
- number: "610"
  proof:
    path: "problems/610/"
    theorem: "Erdos610.erdos_610"
    state: "axiomatic"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    extra_axioms: ["Erdos610.jmrs_corollary2"]
    sources:
      - "https://www.erdosproblems.com/forum/thread/610#post-5678"
      - "https://www.ulam.ai/research/erdos610.lean"
- number: "613"
  proof:
    path: "problems/613/"
    theorem: "Erdos613.erdos_613"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.29.1"
    mathlib_revision: "5e932f97dd25535344f80f9dd8da3aab83df0fe6"
    sources:
      - "https://www.erdosproblems.com/forum/thread/613#post-1678"
      - "https://github.com/teorth/analysis/blob/main/Analysis/Misc/erdos_613.lean"
- number: "618"
  proof:
    path: "problems/618/"
    theorem: "Erdos618.erdos_618"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/618#post-4235"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos618.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos134.lean"
- number: "619"
  proof:
    path: "problems/619/"
    theorem: "Erdos619.erdos_619"
    state: "complete"
    last_update: "2026-06-22"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/619#post-6986"
      - "https://github.com/nick-kuhn/erdos-619"
- number: "621"
  proof:
    path: "problems/621/"
    theorem: "Erdos621.erdos_621"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/621#post-5605"
      - "https://gist.github.com/LorenzoLuccioli/71247a0c86fa35cb1e000160baef0bba#file-erdos621-lean"
- number: "639"
  proof:
    path: "problems/639/"
    theorem: "Erdos639.erdos_639"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/639#post-6189"
      - "https://gist.github.com/Parcly-Taxel/f9a6a963d1057880633e4034294aa98e#file-erdos639-lean"
- number: "645"
  proof:
    path: "problems/645/"
    theorem: "Erdos645.erdos_645"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/645#post-1795"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos645.lean"
- number: "646"
  proof:
    path: "problems/646/"
    theorem: "Erdos646.erdos_646"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/646#post-4507"
- number: "648"
  proof:
    path: "problems/648/"
    theorem: "Erdos648.erdos_648"
    state: "complete"
    last_update: "2026-06-11"
    lean_toolchain: "leanprover/lean4:v4.30.0"
    mathlib_revision: "c5ea00351c28e24afc9f0f84379aa41082b1188f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/648#post-4156"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos648.lean"
      - "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd"
- number: "649"
  proof:
    path: "problems/649/"
    theorem: "Erdos649.erdos_649"
    state: "complete"
    last_update: "2026-05-31"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/649#post-4229"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos649.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos368b.lean"
- number: "650"
  proof:
    path: "problems/650/"
    theorem: "Erdos650.erdos_650"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/650#post-4683"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem650.lean"
- number: "658"
  proof:
    path: "problems/658/"
    theorem: "Erdos658.erdos_658"
    state: "complete"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/658#post-5677"
      - "https://gist.github.com/JohnEdwardJennings/ca7d49761fb51d28613bafc956742fbc#file-erdos658-lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos658.lean"
- number: "659"
  proof:
    path: "problems/659/"
    theorem: "Erdos659.erdos_659"
    state: "axiomatic"
    extra_axioms: ["Erdos659.bernays"]
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/659#post-3156"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos659.lean"
- number: "666"
  proof:
    path: "problems/666/"
    theorem: "Erdos666.erdos_666"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/666#post-4221"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos666.lean"
- number: "674"
  proof:
    path: "problems/674/"
    theorem: "Erdos674.erdos_674"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/674#post-2118"
- number: "678"
  proof:
    path: "problems/678/"
    theorem: "Erdos678.erdos_678"
    state: "complete"
    last_update: "2026-06-11"
    lean_toolchain: "leanprover/lean4:v4.30.0"
    mathlib_revision: "c5ea00351c28e24afc9f0f84379aa41082b1188f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/678#post-2855"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos678.lean"
      - "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd"
- number: "692"
  proof:
    path: "problems/692/"
    theorem: "Erdos692.erdos_692"
    state: "complete"
    last_update: "2026-05-30"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/692#post-5204"
      - "https://gist.github.com/pitmonticone/96516af9100a37a1da81908dc0b0410c#file-erdos692-lean"
- number: "694"
  proof:
    path: "problems/694/"
    theorem: "Erdos694.erdos_694"
    state: "complete"
    last_update: "2026-08-26"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/694#post-6202"
      - "https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P694/Proof.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos694.lean"
      - "https://github.com/frenzymath/FormalPantheon/tree/main/BoundedGaps"
- number: "696"
  proof:
    path: "problems/696/"
    theorem: "Erdos696.erdos_696"
    state: "axiomatic"
    extra_axioms: ["Erdos696.siegel_walfisz"]
    last_update: "2026-06-04"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/696#post-6155"
      - "https://github.com/davidturturean/erdos-696"
- number: "698"
  proof:
    path: "problems/698/"
    theorem: "Erdos698.erdos_698"
    state: "complete"
    last_update: "2026-05-31"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/698#post-3276"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem698.lean"
- number: "707"
  proof:
    path: "problems/707/"
    theorem: "Erdos707.erdos_707"
    state: "complete"
    last_update: "2026-05-31"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/707#post-1350"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos707.lean"
- number: "716"
  proof:
    path: "problems/716/"
    theorem: "Erdos716.erdos_716"
    state: "complete"
    last_update: "2026-06-21"
    lean_toolchain: "leanprover/lean4:v4.30.0"
    mathlib_revision: "c5ea00351c28e24afc9f0f84379aa41082b1188f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/716#post-7096"
- number: "728"
  proof:
    path: "problems/728/"
    theorem: "Erdos728.erdos_728"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/728#post-2828"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos728b.lean"
- number: "729"
  proof:
    path: "problems/729/"
    theorem: "Erdos729.erdos_729"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/729#post-2899"
- number: "741"
  proof:
    path: "problems/741/"
    theorem: "Erdos741.erdos_741"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/741#post-5489"
      - "https://www.erdosproblems.com/forum/thread/741#post-5135"
      - "https://github.com/google-deepmind/formal-conjectures/blob/9d492049e42167b0d2fd58a9e91da3bf160172b5/FormalConjectures/ErdosProblems/741.lean#L228"
      - "https://github.com/mo271/formal-conjectures/blob/486bc8afae062b6711cd16d3466d651ee2880a52/FormalConjectures/ErdosProblems/741.lean#L1630"
- number: "750"
  proof:
    path: "problems/750/"
    theorem: "Erdos750.erdos_750"
    state: "complete"
    last_update: "2026-08-26"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/750#post-6255"
      - "https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P750/Proof_v4.28.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos750.lean"
- number: "751"
  proof:
    path: "problems/751/"
    theorem: "Erdos751.erdos_751"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.23.0"
    mathlib_revision: "37df177aaa770670452312393d4e84aaad56e7b6"
    sources:
      - "https://www.erdosproblems.com/forum/thread/751#post-3835"
      - "https://github.com/SpringSense-Innovation-Institute/ai-for-math-lean/tree/main/erdos-problems/erdos751"
- number: "753"
  proof:
    path: "problems/753/"
    theorem: "Erdos753.erdos_753"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/753#post-5373"
      - "https://gist.github.com/madeve-unipi/80eaf8008c7c798b4f7b5baeb8c1812b#file-erdos753-lean"
- number: "756"
  proof:
    path: "problems/756/"
    theorem: "Erdos756.erdos_756"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/756#post-4792"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem756.lean"
- number: "760"
  proof:
    path: "problems/760/"
    theorem: "Erdos760.erdos_760"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/760#post-5727"
      - "https://gist.github.com/madeve-unipi/a7ae50d445f95e73c360f442c3c84143#file-erdos760-lean"
- number: "762"
  proof:
    path: "problems/762/"
    theorem: "Erdos762.erdos_762"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/762#post-4237"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos762.lean"
- number: "765"
  proof:
    path: "problems/765/"
    theorem: "Erdos765.erdos_765"
    state: "complete"
    last_update: "2026-06-11"
    lean_toolchain: "leanprover/lean4:v4.30.0"
    mathlib_revision: "c5ea00351c28e24afc9f0f84379aa41082b1188f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/765#post-6480"
      - "https://gist.github.com/Parcly-Taxel/13d3bd0f1390b0832a42994a09cf91c5#file-erdos765-lean"
      - "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd"
- number: "775"
  proof:
    path: "problems/775/"
    theorem: "Erdos775.erdos_775"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.28.1"
    mathlib_revision: "1f9fffd5ff0b854b8a1f1f69adc11c61f05f2515"
    sources:
      - "https://www.erdosproblems.com/forum/thread/775#post-5619"
      - "https://gist.github.com/LorenzoLuccioli/dc7dac92dff47aac05b50f2562dbe8c1#file-erdos775-lean"
- number: "785"
  proof:
    path: "problems/785/"
    theorem: "Erdos785.erdos_785"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/785#post-4642"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem785.lean"
- number: "793"
  proof:
    path: "problems/793/"
    theorem: "Erdos793.erdos_793"
    state: "complete"
    last_update: "2026-07-22"
    lean_toolchain: "leanprover/lean4:v4.30.0"
    mathlib_revision: "c5ea00351c28e24afc9f0f84379aa41082b1188f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/793#post-7621"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem793.lean"
- number: "794"
  proof:
    path: "problems/794/"
    theorem: "Erdos794.erdos_794"
    state: "complete"
    last_update: "2026-06-02"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/794#post-4200"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos794.lean"
- number: "798"
  proof:
    path: "problems/798/"
    theorem: "Erdos798.erdos_798"
    state: "complete"
    last_update: "2026-06-03"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/798#post-6329"
      - "https://gist.github.com/Parcly-Taxel/757ca8323d74784da1a776795b9c90a9#file-erdos798-lean"
- number: "818"
  proof:
    path: "problems/818/"
    theorem: "Erdos818.erdos_818"
    state: "complete"
    last_update: "2026-06-03"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/818#post-5890"
      - "https://gist.github.com/tomaz1502/d8f3632157bae289e5d0ed68ccdc9433#file-erdos_818-lean"
- number: "844"
  proof:
    path: "problems/844/"
    theorem: "Erdos844.erdos_844"
    state: "complete"
    last_update: "2026-06-03"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/844#post-5919"
      - "https://gist.github.com/JohnEdwardJennings/e32f2c412b0225091e7519d60741bd2d#file-erdos844-lean"
- number: "845"
  proof:
    path: "problems/845/"
    theorem: "Erdos845.erdos_845"
    state: "complete"
    last_update: "2026-06-03"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/845#post-3601"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem845.lean"
- number: "846"
  proof:
    path: "problems/846/"
    theorem: "Erdos846.erdos_846"
    state: "complete"
    last_update: "2026-06-03"
    lean_toolchain: "leanprover/lean4:v4.22.0"
    mathlib_revision: "79e94a093aff4a60fb1b1f92d9681e407124c2ca"
    sources:
      - "https://www.erdosproblems.com/forum/thread/846#post-4447"
      - "https://github.com/google-deepmind/formal-conjectures/blob/2404258180688283e5141021c75464dc2acfb798/FormalConjectures/ErdosProblems/846.lean"
- number: "862"
  proof:
    path: "problems/862/"
    theorem: "Erdos862.erdos_862"
    state: "complete"
    last_update: "2026-06-11"
    lean_toolchain: "leanprover/lean4:v4.30.0"
    mathlib_revision: "c5ea00351c28e24afc9f0f84379aa41082b1188f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/862#post-3596"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos862.lean"
      - "https://www.erdosproblems.com/forum/thread/43#post-2354"
      - "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd"
- number: "865"
  proof:
    path: "problems/865/"
    theorem: "Erdos865.erdos_865"
    state: "complete"
    last_update: "2026-07-06"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/865#post-7378"
      - "https://github.com/mrricky22/erdos-865-lean"
- number: "867"
  proof:
    path: "problems/867/"
    theorem: "Erdos867.erdos_867"
    state: "complete"
    last_update: "2026-06-03"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/867#post-5279"
      - "https://gist.github.com/pitmonticone/5c1b173e3140f869d7425d8f1003ac70#file-erdos867-lean"
- number: "871"
  proof:
    path: "problems/871/"
    theorem: "Erdos871.erdos_871"
    state: "complete"
    last_update: "2026-06-03"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/871#post-2733"
- number: "884"
  proof:
    path: "problems/884/"
    theorem: "Erdos884.erdos_884"
    state: "complete"
    last_update: "2026-07-23"
    lean_toolchain: "leanprover/lean4:v4.31.0"
    mathlib_revision: "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/884#post-7362"
      - "https://github.com/honicky/erdos884"
- number: "897"
  proof:
    path: "problems/897/"
    theorem: "Erdos897.erdos_897"
    state: "complete"
    last_update: "2026-06-03"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/897#post-2471"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos897.lean"
- number: "898"
  proof:
    path: "problems/898/"
    theorem: "Erdos898.erdos_898"
    state: "complete"
    last_update: "2026-06-05"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/898#post-3882"
- number: "904"
  proof:
    path: "problems/904/"
    theorem: "Erdos904.erdos_904"
    state: "complete"
    last_update: "2026-06-05"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/904#post-5573"
      - "https://gist.github.com/Parcly-Taxel/876d4eadd49a0d29db91ed2e790db733#file-e904-lean"
- number: "905"
  proof:
    path: "problems/905/"
    theorem: "Erdos905.erdos_905"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/905#post-5276"
- number: "907"
  proof:
    path: "problems/907/"
    theorem: "Erdos907.erdos_907"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/907#post-5277"
      - "https://gist.github.com/pitmonticone/f419ac0a78259498f93fd60d49c0b3ea#file-erdos907-lean"
- number: "914"
  proof:
    path: "problems/914/"
    theorem: "Erdos914.erdos_914"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/914#post-5403"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem914.lean"
- number: "923"
  proof:
    path: "problems/923/"
    theorem: "Erdos923.erdos_923"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/923#post-5628"
      - "https://gist.github.com/Parcly-Taxel/28b95db1e5d3e77077d30c07afc55992#file-e923-aristotle-lean"
- number: "927"
  proof:
    path: "problems/927/"
    theorem: "Erdos927.erdos_927"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/927#post-6850"
      - "https://gist.github.com/JohnEdwardJennings/24c9debc9854cb118fbc1314c70941c3#file-erdos927-lean"
- number: "947"
  proof:
    path: "problems/947/"
    theorem: "Erdos947.erdos_947"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/947#post-4068"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem947.lean"
- number: "958"
  proof:
    path: "problems/958/"
    theorem: "Erdos958.erdos_958"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/958#post-2470"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos958.lean"
- number: "964"
  proof:
    path: "problems/964/"
    theorem: "Erdos964.erdos_964"
    state: "complete"
    last_update: "2026-08-27"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/964#post-4280"
      - "https://github.com/danielchin/proofs/blob/main/Proofs/ErdosProblems/Erdos964.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos964.lean"
      - "https://github.com/frenzymath/FormalPantheon/tree/main/BoundedGaps"
- number: "966"
  proof:
    path: "problems/966/"
    theorem: "Erdos966.erdos_966"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/966#post-4472"
- number: "967"
  proof:
    path: "problems/967/"
    theorem: "Erdos967.erdos_967"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/967#post-2303"
      - "https://gist.github.com/llllvvuu/d25f037d1f1000bdabd6ca928c74c9bb#file-967-lean"
- number: "974"
  proof:
    path: "problems/974/"
    theorem: "Erdos974.erdos_974"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.28.1"
    mathlib_revision: "1f9fffd5ff0b854b8a1f1f69adc11c61f05f2515"
    sources:
      - "https://www.erdosproblems.com/forum/thread/974#post-5944"
      - "https://gist.github.com/Parcly-Taxel/a44cbf9a214a5358bf584d05265aec4c#file-erdos974-lean"
- number: "990"
  proof:
    path: "problems/990/"
    theorem: "Erdos990.erdos_990"
    state: "complete"
    last_update: "2026-06-06"
    lean_toolchain: "leanprover/lean4:v4.28.1"
    mathlib_revision: "1f9fffd5ff0b854b8a1f1f69adc11c61f05f2515"
    sources:
      - "https://www.erdosproblems.com/forum/thread/990#post-5312"
      - "https://github.com/yuta0x89/ErdosProblems/blob/main/Erdos990.lean"
- number: "997"
  proof:
    path: "problems/997/"
    theorem: "Erdos997.erdos_997"
    state: "axiomatic"
    extra_axioms: ["Erdos997.maynardTaoBFT"]
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.28.1"
    mathlib_revision: "1f9fffd5ff0b854b8a1f1f69adc11c61f05f2515"
    sources:
      - "https://www.erdosproblems.com/forum/thread/997#post-5189"
      - "https://gist.github.com/pitmonticone/016f2ed66b4cd1c4c4b9998095170e60#file-erdos997-lean"
- number: "1000"
  proof:
    path: "problems/1000/"
    theorem: "Erdos1000.erdos_1000"
    state: "complete"
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1000#post-2509"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1000.lean"
- number: "1007"
  proof:
    path: "problems/1007/"
    theorem: "Erdos1007.erdos_1007"
    state: "complete"
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1007#post-3461"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1007.lean"
- number: "1008"
  proof:
    path: "problems/1008/"
    theorem: "Erdos1008.erdos_1008"
    state: "complete"
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1008#post-3299"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1008c.lean"
- number: "1014"
  proof:
    path: "problems/1014/"
    theorem: "Erdos1014.erdos_1014"
    state: "complete"
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.29.0"
    mathlib_revision: "8a178386ffc0f5fef0b77738bb5449d50efeea95"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1014#post-5751"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.29.0/ErdosProblems/Erdos1014.lean"
- number: "1022"
  proof:
    path: "problems/1022/"
    theorem: "Erdos1022.erdos_1022"
    state: "complete"
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1022#post-3654"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1022.lean"
- number: "1023"
  proof:
    path: "problems/1023/"
    theorem: "Erdos1023.erdos_1023"
    state: "complete"
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1023#post-4251"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1023.lean"
- number: "1026"
  proof:
    path: "problems/1026/"
    theorem: "Erdos1026.erdos_1026"
    state: "complete"
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1026#post-2094"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1026.lean"
- number: "1028"
  proof:
    path: "problems/1028/"
    theorem: "Erdos1028.erdos_1028"
    state: "complete"
    last_update: "2026-06-07"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1028#post-3451"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1028.lean"
- number: "1034"
  proof:
    path: "problems/1034/"
    theorem: "Erdos1034.erdos_1034"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1034#post-2019"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1034.lean"
- number: "1036"
  proof:
    path: "problems/1036/"
    theorem: "Erdos1036.erdos_1036"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1036#post-3561"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1036.lean"
- number: "1037"
  proof:
    path: "problems/1037/"
    theorem: "Erdos1037.erdos_1037"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1037#post-3422"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1037.lean"
- number: "1043"
  proof:
    path: "problems/1043/"
    theorem: "Erdos1043.erdos_1043"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1043#post-2507"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1043.lean"
- number: "1044"
  proof:
    path: "problems/1044/"
    theorem: "Erdos1044.erdos_1044"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1044#post-6012"
      - "https://gist.github.com/LorenzoLuccioli/c3ace69881872112109a6c31b7a87cfc#file-erdos1044-lean"
- number: "1047"
  proof:
    path: "problems/1047/"
    theorem: "Erdos1047.erdos_1047"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1047#post-3595"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1047.lean"
- number: "1048"
  proof:
    path: "problems/1048/"
    theorem: "Erdos1048.erdos_1048"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1048#post-3847"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1048.lean"
- number: "1051"
  proof:
    path: "problems/1051/"
    theorem: "Erdos1051.erdos_1051"
    state: "complete"
    last_update: "2026-08-05"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1051#post-3931"
- number: "1067"
  proof:
    path: "problems/1067/"
    theorem: "Erdos1067.erdos_1067"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1067#post-3898"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1067.lean"
- number: "1071"
  proof:
    path: "problems/1071/"
    theorem: "Erdos1071.erdos_1071"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1071#post-3929"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1071.lean"
      - "https://www.erdosproblems.com/forum/thread/1071#post-4272"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1071b.lean"
- number: "1080"
  proof:
    path: "problems/1080/"
    theorem: "Erdos1080.erdos_1080"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1080#post-2529"
      - "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1080.lean"
- number: "1090"
  proof:
    path: "problems/1090/"
    theorem: "Erdos1090.erdos_1090"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1090#post-4523"
- number: "1098"
  proof:
    path: "problems/1098/"
    theorem: "Erdos1098.erdos_1098"
    state: "complete"
    last_update: "2026-06-10"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1098#post-5863"
      - "https://gist.github.com/JohnEdwardJennings/783dce98df9fa6c333c24617ef07403b#file-erdos1098-lean"
- number: "1102"
  proof:
    path: "problems/1102/"
    theorem: "Erdos1102.erdos_1102"
    state: "complete"
    last_update: "2026-06-12"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "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"
- number: "1112"
  proof:
    path: "problems/1112/"
    theorem: "Erdos1112.erdos_1112"
    state: "complete"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1112#post-7375"
      - "https://github.com/beetree/math_erdos_1112/tree/main/lean"
- number: "1121"
  proof:
    path: "problems/1121/"
    theorem: "Erdos1121.erdos_1121"
    state: "complete"
    last_update: "2026-06-12"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1121#post-5504"
- number: "1125"
  proof:
    path: "problems/1125/"
    theorem: "Erdos1125.erdos_1125"
    state: "complete"
    last_update: "2026-06-12"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1125#post-5332"
      - "https://gist.github.com/ster-oc/18384e6202ffe054cbc76ff2d0b1afde#file-erdos1125-lean"
- number: "1126"
  proof:
    path: "problems/1126/"
    theorem: "Erdos1126.erdos_1126"
    state: "complete"
    last_update: "2026-06-12"
    lean_toolchain: "leanprover/lean4:v4.24.0"
    mathlib_revision: "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1126#post-4524"
- number: "1134"
  proof:
    path: "problems/1134/"
    theorem: "Erdos1134.erdos_1134"
    state: "complete"
    last_update: "2026-06-22"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1134#post-7068"
      - "https://github.com/AxiomMath/erdos-public/blob/main/Erdos/Erdos1134/solution.lean"
- number: "1136"
  proof:
    path: "problems/1136/"
    theorem: "Erdos1136.erdos_1136"
    state: "complete"
    last_update: "2026-06-20"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1136#post-5688"
      - "https://github.com/Woett/Lean-files/blob/main/ErdosProblem1136.lean"
- number: "1138"
  proof:
    path: "problems/1138/"
    theorem: "Erdos1138.erdos_1138"
    state: "complete"
    last_update: "2026-06-20"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1138#post-6243"
      - "https://gist.github.com/LorenzoLuccioli/c7fbdd9809a616974b5587ee526c163b#file-erdos1138-lean"
- number: "1141"
  proof:
    path: "problems/1141/"
    theorem: "Erdos1141.erdos_1141"
    state: "complete"
    last_update: "2026-08-25"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1141#post-5335"
      - "https://github.com/yuta0x89/ErdosProblems/blob/main/Erdos1141.lean"
      - "https://github.com/Woett/Lean-files/blob/main/MertensThird.lean"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos1141.lean"
      - "https://github.com/frenzymath/FormalPantheon/tree/main/BoundedGaps"
- number: "1148"
  proof:
    path: "problems/1148/"
    theorem: "Erdos1148.erdos_1148"
    state: "complete"
    last_update: "2026-08-26"
    lean_toolchain: "leanprover/lean4:v4.33.0"
    mathlib_revision: "db584cd6d46c92f209a44c0f1c829460d327499d"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1148#post-4849"
      - "https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos1148.lean"
- number: "1190"
  proof:
    path: "problems/1190/"
    theorem: "Erdos1190.erdos_1190"
    state: "complete"
    last_update: "2026-06-21"
    lean_toolchain: "leanprover/lean4:v4.27.0"
    mathlib_revision: "a3a10db0e9d66acbebf76c5e6a135066525ac900"
    sources:
      - "https://www.erdosproblems.com/forum/thread/202#post-6456"
      - "https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P1190/Proof_flat.lean"
- number: "1193"
  proof:
    path: "problems/1193/"
    theorem: "Erdos1193.erdos_1193"
    state: "complete"
    last_update: "2026-06-21"
    lean_toolchain: "leanprover/lean4:v4.28.0"
    mathlib_revision: "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1193#post-5360"
      - "https://gist.github.com/pitmonticone/c2658d464f8f5ca0e7fa40ed6fb78a5d"
- number: "1196"
  proof:
    path: "problems/1196/"
    theorem: "Erdos1196.erdos_1196"
    state: "complete"
    last_update: "2026-06-21"
    lean_toolchain: "leanprover/lean4:v4.30.0-rc1"
    mathlib_revision: "f369f66ea08e49c46a2fffaceb6699e6bef11555"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1196#post-5469"
      - "https://github.com/math-inc/Erdos1196"
- number: "1197"
  proof:
    path: "problems/1197/"
    theorem: "Erdos1197.erdos_1197"
    state: "complete"
    last_update: "2026-06-21"
    lean_toolchain: "leanprover/lean4:v4.30.0"
    mathlib_revision: "c5ea00351c28e24afc9f0f84379aa41082b1188f"
    sources:
      - "https://www.erdosproblems.com/forum/thread/1197#post-5409"
      - "https://github.com/Tomodovodoo/Erdos_1197"