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

Groups > comp.theory > #144120

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

Cross-posted to 3 groups.

Show all headers | View raw

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

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