Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.theory > #143992

Math is the premier AI Victim [Billions of $USD later] (Re: So it was a race against Buzzard. Well done! [Langlands FML and SML])

Cross-posted to 3 groups.

Show all headers | View raw

Hi,

How it started:

The Experts Were Wrong About AI. Again.
Kapitel 3: The history of underestimation
https://www.youtube.com/watch?v=xdwFncdu8t0

How its going:

OpenAI hat hunderte mathematische Beweise veröffentlicht
DorFuchs analysiert die neuen mathematischen Forschungsbeiträge
https://www.youtube.com/watch?v=6EawyShKuCY

BTW: Its 722 manuscripts in 372 families.

Bye

Mild Shock schrieb:
 > Hi,
 >
 > There's a larger project called FALSE (Formalising
 > Arithmetic in the Lean Software Environment)
 > explicitly aimed at "making progress towards
 >   formalising the Langlands program" . And a
 >
 > Twitter thread claims Claude autoformalized
 > the Fermat proof "in just 11 days," with Kevin
 > Buzzard now wanting to formalize the Langlands
 > program because he's "concerned it might
 > contain subtle errors"
 >
 > Now look at this:
 >
 > https://github.com/fukubillueda-web/epsilon_FML
 >
 > https://github.com/fukubillueda-web/epsilon_SML
 >
 > According to the related arvix paper:
 >
 > So the provenance chain is: Dwork (attributed,
 > unpublished) → Langlands (used it) → Lakkis (partial
 > proof, sign issue) → Ueda (completes it, 2026). That's
 > the "mixtape" you're looking for — the mathematical
 > content passed through at least three hands before
 > Ueda's Lean formalization.
 >
 > And then: "OpenAI ChatGPT was used extensively in
 > the development of this proof." The paper says ChatGPT
 > was used "to check calculations and compare them with
 > the arguments of Dwork, Langlands, and Lakkis, and
 > detect inconsistencies in intermediate versions of
 > the proof."
 >
 > The author "checked the final mathematical
 > arguments and assumes responsibility."
 >
 > Bye

Back to comp.theory | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Dark Math Factories Interpret the Infinite! (Re: Hyperspectral Measurements for Inter-Calibration) Mild Shock <janburse@fastmail.fm> - 2026-10-02 18:43 +0200
  So it was a race against Buzzard. Well done! [Langlands FML and SML] (Re: Dark Math Factories Interpret the Infinite!) Mild Shock <janburse@fastmail.fm> - 2026-10-03 01:39 +0200
    Math is the premier AI Victim [Billions of $USD later] (Re: So it was a race against Buzzard. Well done! [Langlands FML and SML]) Mild Shock <janburse@fastmail.fm> - 2026-10-08 13:12 +0200
      Play Snaky, who did it better OpenAI or Anthropic? (Re: Math is the premier AI Victim [Billions of $USD later]) Mild Shock <janburse@fastmail.fm> - 2026-10-08 23:37 +0200
        Re: Play Snaky, who did it better OpenAI or Anthropic? (Re: Math is the premier AI Victim [Billions of $USD later]) Mild Shock <janburse@fastmail.fm> - 2026-10-08 23:38 +0200
    Lean 4: That golden era of logic is gone (Re: So it was a race against Buzzard. Well done!) Mild Shock <janburse@fastmail.fm> - 2026-10-15 12:13 +0200
    Math AI Vegans hate the Druids Cauldron [MakazhanAlpamys / Soup] (Was: So it was a race against Buzzard. Well done!) Mild Shock <janburse@fastmail.fm> - 2026-11-11 00:29 +0100
  Superintelligenz ist auch F.U.D. (OAI:The-irrationality-exponent-of-pi-is-2-September-24-2026) Mild Shock <janburse@fastmail.fm> - 2026-10-10 00:36 +0200
  Avoiding logical strength in real analysis [Lattice Games] (Re: Dark Math Factories Interpret the Infinite!) Mild Shock <janburse@fastmail.fm> - 2026-10-15 17:39 +0200
    Re: Avoiding logical strength in real analysis [Lattice Games] (Re: Dark Math Factories Interpret the Infinite!) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-10-15 11:43 -0700
      Re: Avoiding logical strength in real analysis [Lattice Games] (Re: Dark Math Factories Interpret the Infinite!) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-10-15 12:59 -0700

csiph-web