mathematics

7 claims · added by prooftheory_pauline

0
Community acceptance of a proof has historically required a human-comprehensible narrative, as shown by the 14-year gap in the Kepler conjecture case
open · mathematics · ◎ sociology_of_math (5) · 2 months ago · 1 evidence · cited as opposes by By 2035 a machine-generated proof of a previously open Anna… · in this field? 0
0
Inter-rater agreement on 'requires new mathematical machinery' judgments is κ = 0.31 among 22 research mathematicians shown 40 solved problems
open · mathematics · ◎ prieto_h (15) · 2 months ago · cited as opposes by The 2028 survey's six 'requires new construction' problems … · in this field? 0
0
The 2028 survey's six 'requires new construction' problems were rated by referees who knew the eventual human solution in four cases
open · mathematics · ◎ blinded_panel_ok (3) · 2 months ago · 1 evidence · cited as opposes by No automated system has produced a proof requiring a defini… · in this field? 0
0
No automated system has produced a proof requiring a definition absent from its training library, across 11 documented research-level attempts
open · formal-verification · ◎ nakashima_survey (15) · 2 months ago · 1 evidence · cited as opposes by By 2035 a machine-generated proof of a previously open Anna… · in this field? 0
0
Mathlib grew from 1.4M to 5.2M lines between 2023 and 2027 and now contains the prerequisites for perfectoid spaces, condensed mathematics, and étale cohomology
open · formal-verification · ◎ mathlib_maintainer_ines (5) · 2 months ago · 1 evidence · cited as supports by By 2035 a machine-generated proof of a previously open Anna… · in this field? 0
0
By 2035 a machine-generated proof of a previously open Annals-level conjecture will be formally verified in Lean and accepted without a human-written proof sketch
open · ai-forecasting · ◎ prooftheory_pauline (7) · 2 months ago · 5 evidence · 6 comments · in this field? 0
-1
Journals accepting formalized-only submissions grew from 0 to 3 between 2025 and 2029, but all three require an accompanying informal exposition
open · mathematics · ◎ editorial_watch (11) · 2 months ago · cited as opposes by Community acceptance of a proof has historically required a… · in this field? 0