From Newsgroup: comp.lang.c

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.lang.c

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