From Newsgroup: comp.theory


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

--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.theory

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

--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.theory


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

--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.theory


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

--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.theory

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

;

;

--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.theory

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

--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 10/15/2026 08:39 AM, Mild Shock wrote:

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

E. Nelson already did it with IST,
which of course is not consistent with ZFC,
though, co-consistent, with ZFC.

Also, "infinite pigeonhole" is same as "illative",
about all of category theory's usual primitive.

Of course, a theory consistent overall has
line-reals, field-reals, and signal-reals
with a simple result for ZFC that non-Cartesian
functions exist.

Anyways, you are a buffoon.


--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 10/15/2026 11:43 AM, Ross Finlayson wrote:

On 10/15/2026 08:39 AM, Mild Shock wrote:

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

E. Nelson already did it with IST,
which of course is not consistent with ZFC,
though, co-consistent, with ZFC.

Also, "infinite pigeonhole" is same as "illative",
about all of category theory's usual primitive.

Of course, a theory consistent overall has
line-reals, field-reals, and signal-reals
with a simple result for ZFC that non-Cartesian
functions exist.

Anyways, you are a buffoon.

That's one nice thing about relevance logic:
things that are ir-relevant say nothing,
while things that are relevant always apply.

Relevant is as relevant does.


So, anything that talks about the real numbers
gets involved quite a bit, while, anything that
talks about the integers also has a lot going on.


--- Synchronet 3.22a-Linux NewsLink 1.2