Re: Play Snaky, who did it better OpenAI or Anthropic? (Re: Math is the premier AI Victim [Billions of $USD later])

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	comp.theory, comp.lang.c, comp.lang.c++
Subject	Re: Play Snaky, who did it better OpenAI or Anthropic? (Re: Math is the premier AI Victim [Billions of $USD later])
Date	2026-10-08 23:38 +0200
Message-ID	<11a92gd$15avn$5@solani.org> (permalink)
References	<119omv2$pkou$5@solani.org> <119pfap$nbsg$2@solani.org> <11a7tqg$11os2$3@solani.org> <11a92fn$15avn$4@solani.org>

Cross-posted to 3 groups.

Show all headers | View raw

P.S.: BTW they bloody proved a new matrix multiplication,
with asympthotic upper bound showing that ω ≤ 2.25 over
the complex numbers. And Roth irraltionality pi=2. Dang

Mild Shock schrieb:
> Hi,
> 
> The game is among the 722 manuscripts for some
> reasons. Its among the Lean formulations. And
> OpenAI has even fleshed out a big Lean library
> 
> for all their Tensor juggling. The 722
> manuscripts originally annouced here:
> 
> First look at mathematics manuscripts
> from an internal frontier model at OpenAI
> https://community.openai.com/t/1403886
> 
> The game was given a GUI here. But this time
> Claude Opus heavily drove this work:
> 
> OpenAI’s 21-move one, though their strategy
> closed the last three positions my search hadn’t
> https://snaky.gotrevor.org/
> 
> Bye
> 
> Mild Shock schrieb:
>>
>> 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
>

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

csiph-web