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

Groups > comp.lang.prolog > #15956

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 sci.logic, comp.lang.prolog, sci.math
Subject 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:36 +0200
Message-ID <11a92d2$15avn$2@solani.org> (permalink)
References (6 earlier) <10ssije$13umd$3@solani.org> <11478b2$fv28$2@solani.org> <119omnu$pkou$2@solani.org> <119pf8i$nbsg$1@solani.org> <11a7tpe$11os2$2@solani.org>

Cross-posted to 3 groups.

Show all headers | View raw

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

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

Thread

😂 "Plog-like" - that should be the official term! Mild Shock <janburse@fastmail.fm> - 2025-10-08 01:14 +0200
  How deep seek went bonkers (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-10-08 01:23 +0200
  Declarative farts versus MSI Claw AI+, who would win? (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-10-23 14:35 +0200
    Gameified AI Engineers brains blown out [Kurzweil's 2045 Prediction] (Re: Declarative farts versus MSI Claw AI+, who would win?) Mild Shock <janburse@fastmail.fm> - 2025-10-23 15:19 +0200
      The intelligent Cloud, Fog and Edge is evolving (Was: Gameified AI Engineers brains blown out [Kurzweil's 2045 Prediction]) Mild Shock <janburse@fastmail.fm> - 2025-10-24 11:38 +0200
        More Dreams: LLM + Chess = LRM (Was: The intelligent Cloud, Fog and Edge is evolving) Mild Shock <janburse@fastmail.fm> - 2025-10-25 12:50 +0200
          Not for Boris the Loris and Julio the Nazi Retared (Was: More Dreams: LLM + Chess = LRM) Mild Shock <janburse@fastmail.fm> - 2025-10-25 13:08 +0200
  Arrow Functions can do Existential Quantifier (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:12 +0100
    Resolving Ambiguity in Negation as Failure Re: Arrow Functions can do Existential Quantifier (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:21 +0100
      Future Outlook of Logic Programming (Was: Resolving Ambiguity in Negation as Failure) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:25 +0100
    Clueless Moron and Paid Putin Troll (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:50 +0100
      2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:51 +0100
        Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:52 +0100
          Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:52 +0100
          Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:56 +0100
          Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:58 +0100
            What does Type Free mean? (Re: 2.1 Logical variables and equations) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:59 +0100
      A noiseless patient Spider is a Pussy Mild Shock <janburse@fastmail.fm> - 2025-11-07 00:03 +0100
      Forget your Sputnik Commodore C64 with 8088 [Logic Tiling] (Re: Hyperspectral Measurements for Inter-Calibration) Mild Shock <janburse@fastmail.fm> - 2026-07-27 11:29 +0200
        Train yourself to become a nosomatic AI chirurgeon (Re: Forget your Sputnik Commodore C64 with 8088 [Logic Tiling]) Mild Shock <janburse@fastmail.fm> - 2026-07-27 11:40 +0200
          Homework: Game Engine in WebGPU (Re: Train yourself to become a nosomatic AI chirurgeon) Mild Shock <janburse@fastmail.fm> - 2026-08-03 02:06 +0200
            Johnny Depp prevention [Windows 11 etc...] (Re: Homework: Game Engine in WebGPU) Mild Shock <janburse@fastmail.fm> - 2026-08-03 18:17 +0200
              But how can you deploy, when its ROM? (Re: Johnny Depp prevention [Windows 11 etc...]) Mild Shock <janburse@fastmail.fm> - 2026-08-03 18:21 +0200
              New addition to π-WAM is π-WAM Assembly (Re: Johnny Depp prevention [Windows 11 etc...]) Mild Shock <janburse@fastmail.fm> - 2026-08-09 19:46 +0200
          The future Numa Brains will be gorgeous (Was: Train yourself to become a nosomatic AI chirurgeon) Mild Shock <janburse@fastmail.fm> - 2026-09-25 19:10 +0200
            Estimating P(doom E-graphs) to < 10% (Was: The future Numa Brains will be gorgeous) Mild Shock <janburse@fastmail.fm> - 2026-09-28 14:13 +0200
          Nosomatic AI Chirurgeon: RSI of Use/Mention? (Re: Train yourself to become a nosomatic AI chirurgeon) Mild Shock <janburse@fastmail.fm> - 2026-10-24 12:55 +0200
        Re: Forget your Sputnik Commodore C64 with 8088 [Logic Tiling] (Re: Hyperspectral Measurements for Inter-Calibration) Lane W <cactus_DAC@yahoo.com> - 2026-07-27 08:07 -0600
      Brova you enjoy made up nonsense? [Einstein tech cult] (Re: Hyperspectral Measurements for Inter-Calibration (Re: Logtalk big time salami slicing) Mild Shock <janburse@fastmail.fm> - 2026-07-27 17:08 +0200
        NVIDIA Einstein and Q8.24 RGB Values [Earth and Star Gazers] (Re: Brova you enjoy made up nonsense?) Mild Shock <janburse@fastmail.fm> - 2026-07-27 17:33 +0200
          Just lookup orbital AI and SpaceX (Re: NVIDIA Einstein and Q8.24 RGB Values) Mild Shock <janburse@fastmail.fm> - 2026-07-27 17:38 +0200
        Re: Brova you enjoy made up nonsense? [Einstein tech cult] (Re: Hyperspectral Measurements for Inter-Calibration (Re: Logtalk big time salami slicing) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-27 18:55 -0700
      Ljubljana School versus Zurich School (Re: Prolog PIP-0110: Its a Floating-Point Multiverse? [Stoic Grisu versus Rest of World] (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2026-08-03 20:16 +0200
        Big thanks to Ljubljana School [Searching 0xCAFFEE] (Re: Ljubljana School versus Zurich School) Mild Shock <janburse@fastmail.fm> - 2026-08-03 20:42 +0200
        Peking School versus Ljubljana School [Everything Is a Plugin] (Re: Ljubljana School versus Zurich School) Mild Shock <janburse@fastmail.fm> - 2026-08-21 17:44 +0200
      Dark Math Factories Interpret the Infinite! (Re: Hyperspectral Measurements for Inter-Calibration) Mild Shock <janburse@fastmail.fm> - 2026-10-02 18:39 +0200
        So it was a race against Buzzard. Well done! [Langlands FML and SML] (Was: Dark Math Factories Interpret the Infinite!) Mild Shock <janburse@fastmail.fm> - 2026-10-03 01:37 +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:11 +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:36 +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:37 +0200
          Lean 4: That golden era of logic is gone (Was: So it was a race against Buzzard. Well done!) Mild Shock <janburse@fastmail.fm> - 2026-10-15 12:08 +0200
          Math AI Vegans hate the Druids Cauldron [MakazhanAlpamys / Soup] (Re: So it was a race against Buzzard. Well done!) Mild Shock <janburse@fastmail.fm> - 2026-11-11 00:17 +0100
        An elementary proof or pi irrationality = 2 [Natural Intelligence] Mild Shock <janburse@fastmail.fm> - 2026-10-09 19:39 +0200
          Cont. Now with Integers (Was: An elementary proof or pi irrationality = 2 [Natural Intelligence]) Mild Shock <janburse@fastmail.fm> - 2026-10-09 20:22 +0200
            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:34 +0200
              Time got dilated by Gemini & Deepseek [The new Shalosh B. Ekhad] (Was: Superintelligenz ist auch F.U.D. ) Mild Shock <janburse@fastmail.fm> - 2026-10-10 13:00 +0200
      Avoiding logical strength in real analysis [Lattice Games] (Was: Hyperspectral Measurements for Inter-Calibration) Mild Shock <janburse@fastmail.fm> - 2026-10-15 17:35 +0200
  2025 Obituary: Skew Confluence (aka “Stews” 😆) (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-07 01:38 +0100
    Backdoor Monkeys from Eternal September (Re: 2025 Obituary: Skew Confluence (aka “Stews” 😆)) Mild Shock <janburse@fastmail.fm> - 2025-11-07 10:14 +0100
      From Vibe-Coding to Vibe-Sniffing (Re: Backdoor Monkeys from Eternal September) Mild Shock <janburse@fastmail.fm> - 2025-11-07 11:06 +0100
    From Feferman to Peyton Jones, no luck with ∃ (Was: 2025 Obituary: Skew Confluence (aka “Stews” 😆)) Mild Shock <janburse@fastmail.fm> - 2025-11-08 20:33 +0100
      Taxon (TBox) / Affirm (ABox) was a thing in the 90s? (e: The quantifer ∃ is just the Combinator K (Schönfinkels C)?) Mild Shock <janburse@fastmail.fm> - 2025-11-08 22:30 +0100
  Not Ross Finlayson: Pioneers Cliff B. Jones (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-09 21:18 +0100

csiph-web