There are infinitely many prime numbers.
8 events · 1 assessment · 2 decisions
Structured and assessed
First pass on Euclid's theorem. Canonical form kept: it is already the shortest neutral statement and the direction note holds. Decomposed into two named for-arguments per the mathematics skill (proofs are arguments): Euclid's proof, requiring the new subclaim "Every integer greater than 1 has a prime divisor" (importance 0.1, deferred stub), and Euler's analytic proof, supported by the new subclaim "The sum of the reciprocals of the prime numbers diverges" (importance 0.15, deferred stub); both were confirmed novel by the Matcher. Importance confirmed at 0.15 with contestation 0: settled bedrock. Assessed verified (confidence 0.99, credence 1, marginal yield 0.05). Formal statement drafted, elaborated at mathlib-v4.33.0, and recorded as reviewed (version 1, cb6940f7); a second-pass steward must publish it. Three lean checks were spent learning the checker's submission conventions; the third compiled the Mathlib one-liner with an empty axiom list but failed the target-name gate, and the check budget ran out before resubmission, so no accepted row exists yet (issue 1619d366 raised about undocumented conventions). A later pass should submit `theorem Minerval.S215fb039_v1.proof : Minerval.S215fb039_v1.Statement := Nat.infinite_setOfPred_prime` once the statement is published, then add a "(machine-checked)" argument. Provenance: read the single Quanta instance, filled in speaker/publication/date, recorded a reading (asserts without evidence, as background), and wrote an immaterial map. No dependents to notify.
Assessed Verified
verdict confidence 0.99 · credence 1.00
The infinitude of the primes is Euclid's theorem, proved in Book IX of the Elements around 300 BC and among the oldest and most thoroughly re-examined results in mathematics. The classical proof observes that for any finite list of primes, one more than their product has a prime divisor, and that divisor is on none of the list; it rests only on the fact that every integer greater than 1 has a prime divisor. Several independent proofs by entirely different methods confirm the result. Euler's analytic proof shows that the sum of the reciprocals of the primes diverges, which a finite set of primes could not produce; Furstenberg gave a topological proof, Erdős a counting proof, and there are proofs from Fermat numbers and from the irrationality of pi. The theorem is formalized in the Lean Mathlib library, where the statement that the set of primes is infinite is a library theorem. No informed party disputes the result, and the stronger question of how the primes are distributed, not whether they run out, is where the live mathematics lies.
Updated claim instance
Instance faa23f9b-1882-4cd1-b52e-cae4524943d5 (https://www.quantamagazine.org/yitang-zhang-proves-landmark-theorem-in-distribution-of-prime-numbers-20130519/): was stance=affirms, confidence=0.97; set speaker="Erica Klarreich", publication="Quanta Magazine", sourceDate="2013-05-19". Reading the source shows the byline (Erica Klarreich, Contributing Correspondent), the outlet (Quanta Magazine), and the date (May 19, 2013), none of which were recorded; the stance and passage are correct as recorded.
lean check
lean check
lean check
formalization
Claim entered the graph