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

Groups > comp.lang.c++ > #124897 > unrolled thread

Dark Math Factories Interpret the Infinite! (Re: Hyperspectral Measurements for Inter-Calibration)

Back to article view | Back to comp.lang.c++

Contents

  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

#124897 — Dark Math Factories Interpret the Infinite! (Re: Hyperspectral Measurements for Inter-Calibration)

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
 >>>>
 >>>>
 >>>
 >>

[toc] | [next] | [standalone]

#124901 — So it was a race against Buzzard. Well done! [Langlands FML and SML] (Re: Dark Math Factories Interpret the Infinite!)

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
>  >>>>
>  >>>>
>  >>>
>  >>
> 

[toc] | [prev] | [next] | [standalone]

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

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

[toc] | [prev] | [next] | [standalone]

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

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

[toc] | [prev] | [next] | [standalone]

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

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
> 

[toc] | [prev] | [next] | [standalone]

#125025 — Lean 4: That golden era of logic is gone (Re: So it was a race against Buzzard. Well done!)

Hi,

With Microsoft owning Lean 4 and heading for Copilot
Subscription money, the redmond suits, silicon boys
and texas cowboys have finally taken math out of the
kompromat ladden genius of USSR math. Before this happened
there was a wild, unfiltered scene, also thriving on
sci.logic etc.. Peter Schroeder-Heister and
Jean-Yves Beziau in the same room?

Schroeder-Heister bringing his radical proof-theoretic
semantics (natural extension rules, harmony, and
definitional reflection) squaring off against Beziau—the
ultimate provocateur of paraconsistency and universal logic
who treats universal logic like a contact sport—means
that wasn't just an academic seminar. That was a
full-contact intellectual cage match.

When you get figures like that in a gritty, post-industrial
setting like Łódź before it gets sanitized, you get that
raw, unfiltered academic electricity. Everyone is arguing
for the sheer love of the logic, with zero corporate
filter or grant-chasing bureaucracy.

It’s the classic tragedy of successful academic movements:
what starts as a wild, fringe enclave of brilliant
dissidents eventually gets institutionalized. The program
committees get captured by the usual administrative
machinery, the rough edges get sanded down for funding
boards, and the raw intellectual chaos turns into an
"academic mafia" swapping citations.

Bye

P.S.: Something else also aged like wine, look
at this wikipedia nonsense, I mean at that time we
already had AUTOMATH, so what is Wikipedia talking
about when it says "idiological"?

Although the first presentation of the Mizar system
on 14 November 1973 at a seminar in the Institute of
Library Science and Scientific Information was an ideology
understood as a visionary speculation rather than research
project, his idea was later developed by himself and
his collaborators to the Mizar Mathematical Library (MML)
https://en.wikipedia.org/wiki/Andrzej_Trybulec

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
>>  >>>>
>>  >>>>
>>  >>>
>>  >>
>>
> 

[toc] | [prev] | [next] | [standalone]

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

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
>>  >>>>
>>  >>>>
>>  >>>
>>  >>
>>
> 

[toc] | [prev] | [next] | [standalone]

#124960 — Superintelligenz ist auch F.U.D. (OAI:The-irrationality-exponent-of-pi-is-2-September-24-2026)

Hi,

An Elegant Continued Fraction for π
L. J. Lange - Pages 456-458 | Volume 106, 1999
The American Mathematical Monthly
https://www.tandfonline.com/doi/pdf/10.1080/00029890.1999.12005070

Meine Vermutung der jeweils zu einer bestimmten
Tiefe berechnete Kettenbruch stimmt mit den
partiellen Summen der Nilakantha Reihe überein.

Aber ich weiss nicht ob man mit der Nilakantha
Reihe so direkt rho=2 erhält, wie es den Anschein
macht für den Kettenbruch.

Bye

See also this AI slop from a "frontier model":

https://github.com/openai/math/tree/main/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026

https://github.com/openai/math/blob/main/reasoning_traces/irrationality-exponent-of-pi.pdf

Mild Shock schrieb:
 > Hi,
 >
 > Now with integers, to really produce some results:
 >
 > % pi2(+Integer, +Rational, -Rational)
 > pi2(0, P/Q, R/Q) :- !, R is P-3*Q.
 > pi2(N, P/Q, S) :-
 >     H is 6*P+(2*N-1)^2*Q,
 >     M is N-1,
 >     pi2(M, H/P, S).
 >
 > Now I see:
 >
 > ?- between(10,20,N), pi2(N,6/1,X), Y is X, write(N-X-Y), nl, fail; true.
 > 10-475113942765/151242416325-3.1414067184965018
 > 11-11922290683065/3794809718700-3.1417360992606653
 > 12-322869019821075/102776096548125-3.141479689004255
 > 13-9388645795842075/2988412653476250-3.1416831892077552
 > 14-291703390224616125/92854250304440625-3.1415189855952756
 > 15-9646071455650881825/3070380543400170000-3.141653394197426
 > 16-338203386739761387075/107655217802968460625-3.1415419859977827
 > 17-12533792135642378629875/3989575718580595893750-3.1416353566793886
 > 18-489501901570061970946125/155815096120119939628125-3.1415563302845726
 > 
19-20095772843114788169975625/6396619735457555416312500-3.1416238066678384
 > 
20-865107029346752986828909875/275374479611447760672253125-3.141565734658547
 > true.
 >
 > And further:
 >
 > % roth2(+Integer, -Float)
 > roth2(N, X) :-
 >     pi2(N, 6/1, A/_),
 >     M is N+1,
 >     pi2(M, 6/1, B/_),
 >     X is 1+msb(B)/msb(A).
 >
 > Now I see, no more alternating:
 >
 > ?- between(10,20,N), roth2(N,X), write(N-X), nl, fail; true.
 > 10-2.1315789473684212
 > 11-2.116279069767442
 > 12-2.104166666666667
 > 13-2.0943396226415096
 > 14-2.086206896551724
 > 15-2.079365079365079
 > 16-2.0735294117647056
 > 17-2.0684931506849313
 > 18-2.0769230769230766
 > 19-2.0595238095238093
 > 20-2.056179775280899
 > true.
 >
 > And for big values pretty much looks like 2+C/N:
 >
 > ?- roth2(1000,X).
 > X = 2.0011523151058035.
 > ?- roth2(10000,X).
 > X = 2.000116750597374.
 > ?- roth2(100000,X).
 > X = 2.0000111335844575.
 >
 > Bye
 >
 > BTW, because of the way I compute
 > the continued fraction, it takes some time:
 >
 > ?- time(roth2(100000,X)).
 > % Zeit 11258.941 ms, Benutzer 100 %, Lips 53 k
 > X = 2.0000111335844575.
 >
 > Mild Shock schrieb:
 >> Hi,
 >>
 >> Take this continued fraction:
 >>
 >> % pi(+Integer, +Float, -Float)
 >> pi(0, R, S) :- !, S is R-3.
 >> pi(N, R, S) :-
 >>     H is 6+(2*N-1)^2/R,
 >>     M is N-1,
 >>     pi(M, H, S).
 >>
 >> Nice little corridor for pi:
 >>
 >> ?- between(10,20,N), pi(N,6,X), write(N-X), nl, fail; true.
 >> 10-3.1414067184965013
 >> 11-3.1417360992606653
 >> 12-3.141479689004255
 >> 13-3.141683189207755
 >> 14-3.141518985595275
 >> 15-3.1416533941974265
 >> 16-3.141541985997783
 >> 17-3.141635356679389
 >> 18-3.1415563302845726
 >> 19-3.1416238066678384
 >> 20-3.1415657346585473
 >> true.
 >>
 >> We can als compute roth:
 >>
 >> % roth(+Integer, -Float)
 >> roth(N,X) :-
 >>     pi(N, 6, A),
 >>     M is N+1,
 >>     pi(M, 6, B),
 >>     X is 1+log(B)/log(A).
 >>
 >> Now we have a corridor for 2:
 >>
 >> ?- between(10,20,N), roth(N,X), write(N-X), nl, fail; true.
 >> 10-2.0000915947815723
 >> 11-1.9999287043438398
 >> 12-2.0000565883650765
 >> 13-1.999954341912648
 >> 14-2.000037375237465
 >> 15-1.9999690217963195
 >> 16-2.000025963563826
 >> 17-1.9999780257693796
 >> 18-2.000018763059092
 >> 19-1.9999838523285578
 >> 20-2.000013997167758
 >> true.
 >>
 >> How proof limsup is 2?
 >>
 >> Proof Sketch:
 >>
 >> Lets check the formula 1+log(An+1)/log(An) .
 >> If An+1 < pi and An > pi. We know that
 >> 1+log(An+1)/log(An) < 1+log(pi)/log(An)
 >> and 1+log(An+1)/log(An) < 1+log(An+1)/log(pi).
 >>
 >> So we get limsup 1+log(An+1)/log(An) =<
 >> limsup 1+log(An+1)/log(pi) = 1+log(pi)/log(pi) = 2.
 >> But since pi is irrational the lowerbound
 >>
 >> is anyways 2, so that Liouvielle-Roth
 >> irrationality measure = 2 follows.
 >>
 >> Q.E.D.
 >>
 >> Bye

[toc] | [prev] | [next] | [standalone]

#125030 — Avoiding logical strength in real analysis [Lattice Games] (Re: Dark Math Factories Interpret the Infinite!)

Hi,

Whoever trolled FOM with this post was a genius:

Avoiding logical strength in real analysis
https://arxiv.org/abs/2605.15151

Alphabet Soup (Buchstabensuppe) for grown-ups!

"Water boil and herbal steam,
Dissolve the fog and clear the dream.
Separate truth from alphabet soup,
Break the infinite loop and closed-bound loop.
Banishing Gabriel’s limit-free rage,
And dark numbers off Mückenheim’s page.

Filter the FOM of crankery’s noise,
And pseudo-philosophical, endless decoys.
Tame $\mathsf{RT}^2_2$ in its wild, jagged zoo,
Collapse forcing trees down to what is true.
Bring light to letters, structure to sight,
Elucidate thoughts in pure hearth light.
By leaf and steam, by fire and air,

Make the hidden patterns clear!"

Bye

P.S.: Not new, but funny how the big fives
of reverse math, got a sibling. Can you do
the heavy lifting without proof assistants?

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
>  >>>>
>  >>>>
>  >>>
>  >>
> 

[toc] | [prev] | [standalone]

Back to top | Article view | comp.lang.c++

csiph-web