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

Groups > comp.theory > #145309

Math AI Vegans hate the Druids Cauldron [MakazhanAlpamys / Soup] (Was: So it was a race against Buzzard. Well done!)

Cross-posted to 3 groups.

Show all headers | View raw

Hi,

How it started,

Mathematics of the Future
5.6 AI-vegan mathematicians
https://math.mit.edu/~etingof/futuremath.pdf

How its going:

Soup Layer Streaming for LLM fine-tuning
#4 Repository of the Day
https://github.com/MakazhanAlpamys/Soup

I fear one or two kids might teach it
math (for example via Sutskever/Megill
approach) and soon become new Einsteins,

developing wormhole warpspeed math.

Have Fun

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
> 
> Mild Shock schrieb:
>> Hi,
>>
>> OpenAI has announced enhancing their Math Swarms
>> by an interpretability accelerator prompt recently
>> discovered in a Terrence Tao workshop.
>>
>> So they are now takling:
>>
>> Mathematician W. Hugh Woodin Explains Continuum Hypothesis
>> https://www.youtube.com/watch?v=ZC7wglkBWMM
>>
>> Infinite fun with infinite worlds
>> https://ethz.ch/en/news-and-events/eth-news/news/2020/08/infinite-fun-with-the-infinite-worlds.html 
>>
>>
>> A partial Lean 4 formalization is already in
>> the making. But the hurdles are high. Some
>> speaker of the effort said:
>>
>> The computer might find a new tamagochi knottheory
>> lemma, which will then allow SpaceX to fly through
>> wormholes, but the hurdle will be hight that
>>
>> a single human mathematician mind might
>> ingest, understand and interpret it.
>>
>> Bye
>>
>> Mild Shock schrieb:
>>  > Hi,
>>  >
>>  > Hyperspectral measurements for inter-calibration,
>>  > reached a significant milestone this summer.
>>  >
>>  > The naval observatory only uses fidget spinners
>>  > to measure time, so forget Colorado.
>>  >
>>  > Bye
>>  >
>>  > Ross Finlayson schrieb:
>>  >  >
>>  >  > So, there's at least three accounts of what can define 
>> "measurement of
>>  >  > time", in the micro, meso, and macro.
>>  >  >
>>  >  > Then these days pretty much the world relies on "the naval 
>> observatory
>>  >  > in Colorado" if not so much "the clock tower in Greenwich", as with
>>  >  > regards to ye olde UTC, CUT, "Zulu", and so on, time.
>>  >  >
>>  >  > About relativity theory and "measuring rods and clocks", then, it's
>>  >  > similar that "metric and norm" for "length and distance" also has
>>  >  > about the Planckian what are "iota-values" as it would be, or, 
>> "Pauli
>>  >  > Plancks", or "Dirac's Pauli Plancks", of measuring space, 
>> vis-a-vis,
>>  >  > measuring time.
>>  >  >
>>  >  >
>>  >  > So, there are at least three accounts of what defines measuring 
>> time,
>>  >  > and at least three accounts of what defines measuring space.
>>  >  >
>>  >  >
>>  >  > Then, since relativity theory is defined by what does that,
>>  >  > it has the various ways, to so fulfill doing that.
>>  >  >
>>  >  >
>>  >  > Yeah, I know, most "professional physicists" only have one of those
>>  >  > on their little note-card with which they passed graduate school.
>>  >
>>  > Mild Shock schrieb:
>>  >> Hi,
>>  >>
>>  >> Ross Finlayson schrieb:
>>  >>  > Or shaves pennies.
>>  >>
>>  >>  >>> X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI
>>  >>  >>> processor which combines neural processes with symbolic 
>> reasoning.
>>  >>  >>> https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe
>>  >>
>>  >> Cost/hour: $200,000.00
>>  >>
>>  >> LoL
>>  >>
>>  >> Bye
>>  >>
>>  >> P.S.: If it could do some quant trading magic, one would
>>  >> possibly pay so much. But Logtalk is simply too lame:
>>  >>
>>  >> Version release notes
>>  >> XVM Engine v10.2.4 is the full engine capable of running
>>  >> all XVM and Logtalk programs, excluding for logtalk tools.
>>  >>
>>  >> Mild Shock schrieb:
>>  >>> Hi,
>>  >>>
>>  >>> The 9122171.18175435 is a little offending, what if one
>>  >>> keeps a federal secret after the 6 fraction digit?
>>  >>>
>>  >>> Bye
>>  >>>
>>  >>> Mild Shock schrieb:
>>  >>>> Hi,
>>  >>>>
>>  >>>> Ok, leaving the beaten path of my Prolog system
>>  >>>> probing, and look at some newer beast.
>>  >>>>
>>  >>>> This looks bad:
>>  >>>>
>>  >>>> ?- format('~6f', [pi**14]), nl.
>>  >>>> 9122171.18175435
>>  >>>>
>>  >>>> Expected result:
>>  >>>>
>>  >>>> ?- format('~6f', [pi**14]), nl.
>>  >>>> 9122171.181754
>>  >>>>
>>  >>>> Bye
>>  >>>>
>>  >>>> BTW: Tested using this test tester:
>>  >>>>
>>  >>>> X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI
>> processor which combines neural processes with symbolic reasoning.
>>  >>>> https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe
>>  >>>>
>>  >>>> Mild Shock schrieb:
>>  >>>>  >>> See also:
>>  >>>>  >>> https://prolog-lang.org/ImprovementsForum/0110-format.html
>>  >>>>
>>  >>>>
>>  >>>
>>  >>
>>
> 

Back to comp.theory | Previous — 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