Hacker GitHub

← All repos

plby/lean-proofs

View on GitHub ↗ ★ 47 Lean

Some Lean proofs

3 mentions on Hacker News by 3 people: 0 stories, 3 comments · first 2026-01-10 · latest 2026-01-10

Mentions per year 3 mentions · busiest year 2026 (3)
20082026
AllStoriesComments NewestTopOldest
  1. …The Lean-language statement of the problem (which can be done either by hand or by AI) is (from https://github.com/plby/lean-proofs/blob/f44d8c0e433ab285541... ): ∀ᶠ ε : ℝ in [>] 0, ∀ C > (0 : ℝ), ∀ C' > C, ∃ a b n : ℕ, 0 < n ∧ ε * n < a ∧…
    comment by svat · 2026-01-10 · in “Erdos problem #728 was solved more or less autonomously by AI”
  2. …lines of AI-generated code seems a very good place for some mistake in the translation to sneak in https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/Er... Though I suppose if the problem statement in Lean is human-generated and…
    comment by snowmobile · 2026-01-10 · in “Erdos problem #728 was solved more or less autonomously by AI”
  3. …lean proof? I don't know maybe it's in some random pull request I didn't find. Edit: Found it here https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/Er...
    comment by aziis98 · 2026-01-10 · in “Erdos problem #728 was solved more or less autonomously by AI”