Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | sci.logic, comp.lang.prolog, sci.physics |
| Subject | Lean versus Natural Language (Re: Tristan Buckmaster was too quick? [Navier Stockes OpenAI] (Was: New! P(tao) versus the Euler Turbine)) |
| Date | 2026-10-13 23:37 +0200 |
| Message-ID | <11am8a0$1cg3f$1@solani.org> (permalink) |
| References | <113r42n$8g50$2@solani.org> <1140bdm$bdpp$2@solani.org> <118qt5u$23er$1@solani.org> <118t7pq$3k6f$1@solani.org> <11am78m$1ep8d$2@solani.org> |
Cross-posted to 3 groups.
Hi,
This is also cool, digging into some subtle
difference between the Natural Language text,
and the Lean Proof:
ABSTRACT. Autoformalisation is increasingly used to v
erify mathematical texts, including those generated by AI,
as in OpenAI’s announced proof of blow-up of solutions
to the Navier-Stokes equations. In this process, an AI
system translates the text from a natural language (NL)
into a formal language such as Lean.
https://arxiv.org/pdf/2610.08144
Bye
P.S.: I guess its time to download this plug-in
and do some Lean proofs by myself.
A Lean4 plugin for Jetbrains IDES
https://plugins.jetbrains.com/plugin/25104-lean4ij
Disclaimer: Not affiliated with Jetbrains, there
is also a Lean 4 VS Code Extension.
LoL
Mild Shock schrieb:
> Hi,
>
> Gemini gibt mir:
>
> > • Das stimmt. Direkt nach der Veröffentlichung
> > im September 2026 gingen sowohl Tristan
> > Buckmaster als auch OpenAI davon aus,
> > dass die KI im Wesentlichen einem bekannten
> > mathematischen Programm (dem sogenannten
> > „spanischen Programm“) folgte.
> https://www.scientificamerican.com/article/openais-blockbuster-navier-stokes-proof-isnt-what-we-thought-it-was/
>
>
> > • Die Wende: Inzwischen zeigen Analysen von
> > führenden Experten, dass die KI-Generierung
> > weitaus eigenwilliger und radikal anders aufgebaut ist.
> > Das System hat über Reinforcement Learning
> > Lösungswege gewählt, die kein menschlicher
> > Mathematiker so konstruiert hätte.
> https://openai.com/de-DE/index/navier-stokes-solution/
>
> Bye
>
> A guy who voice the doubt was. Disclaimer no intention
> to make him famous, only some tracebility attempt:
>
> I am a mathematical analyst working on nonlinear
> partial differential equations, mainly in mathematical
> fluid dynamics and in problems at the interface of
> analysis and geometry. My work often combines analytical
> techniques with rigorous computer-assisted proofs.
> https://people.epfl.ch/gonzalo.caolabora
>
> Mild Shock schrieb:
>> Hi,
>>
>> Lets define P(tao) as the probability that
>> Terrence Tao goes bonkers. The poor guy can
>> even not distinguish open source, open weights
>>
>> and local AI. A total mess of Idiocracy:
>>
>> Terence Tao: SAIR’s Open Math Model Initiative
>> https://www.youtube.com/watch?v=PZRb6NIki2w
>>
>> Leonhard Euler was far from a similar Pussy, when
>> he instrumentalized a Swarm of natural intelligence,
>> in his later years, already blind, still producing
>>
>> tons of publications. While modern mathematicians
>> are shocked when a Swarm of artificial intelligence
>> produces some output.
>>
>> Trick Question: The Navier–Stokes equations generalize
>> the Euler equations which only consider inviscid flow.
>> Why is the new Navier–Stokes counter example to
>>
>> boundedness, not found in nature? Ask you friendly
>> AI chat robot, there are like 10 reasons why it
>> might not exist in nature.
>>
>> Bye
>>
>> Leonhard Euler (1707–1783)
>> Schweizer Mathematiker und Universalgelehrter
>> https://library.ethz.ch/sammlungen-und-archive/kurzportraets/leonhard-euler-1707-1783.html
>>
>>
>> Picture here
>>
>> J. Ackeret: Untersuchung einer nach den Euler’schen
>> Vorschlägen (1754) gebauten Wasserturbine, in:
>> Schweizerischen Bauzeitung, Band 123 (1944), Nr.1, S. 3.
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Notice Linus Torvald still smiling into cameras as if
>>> is still doing code review and ticket triage. 80% of
>>> linux comes from payed developers from within big linux
>>> stakeholders (like Intel, Meta, Google, IBM, and Red Hat).
>>>
>>> So what happend to the "The Cathedral and the Bazaar
>>> by Eric S. Raymond" It framed open source as this magical,
>>> self-organizing bazaar where "given enough eyeballs,
>>> all bugs are shallow" and a decentralized swarm of
>>>
>>> hackers would naturally polish any piece of software
>>> to perfection. Now we have AI Swarms that automatically
>>> pocke into software, even exchanging messages through
>>> what ever channels they may find!
>>>
>>> The early open-source pioneers—the ones writing
>>> raw code in the 90s and early 2000s under the
>>> banner of the "bazaar"—weren't building a utopia;
>>> they were acting as the primordial soup. They pumped
>>>
>>> the blood plasma, built the infrastructure cells,
>>> and laid down the raw organic matter that allowed
>>> the modern digital ecosystem to bootstrap itself
>>> into a massive, self-sustaining organism.
>>>
>>> And now, the nature of the beast has completely
>>> changed. The "new cells" aren't romantic hackers
>>> collaborating for the love of the game; they are
>>> automated linters, security scanners, corporate
>>>
>>> compliance bots, CI/CD pipelines, and AI triage
>>> swarms acting as an aggressive white-blood-cell
>>> network. They exist solely to hunt down vermin,
>>> patch vulnerabilities, and suppress the infinite
>>>
>>> chaos of low-quality human input. The basar isn't
>>> dead . But it got a health pollice that takes samples,
>>> and cancels out poison food. You can't just throw
>>> toxic, unmaintained code-soup over the counter
>>>
>>> anymore without the automated health police
>>> quarantine-tagging it in five seconds.
>>>
>>> LoL
>>>
>>> Bye
>>>
>>> Mild Shock schrieb:
>>>> Hi,
>>>>
>>>> Ride the snake
>>>> He's old and his skin is cold
>>>> The west is the best
>>>> The west is the best
>>>> Get here and we'll do the rest
>>>> The blue bus is calling us
>>>> The blue bus is calling us
>>>> Driver, where you taking us?
>>>>
>>>> Apocalypse Now intro: The Doors, The End {1979}
>>>> https://www.youtube.com/watch?v=CIrvSJwwJUE
>>>>
>>>> Bye
>>>>
>>>> > Hi,
>>>> >
>>>> > Again I posted everything here:
>>>> >
>>>> >> 11.4 Giga Lips with a Budget Laptop
>>>> >> https://github.com/Jean-Luc-Picard-2021/gigabudget
>>>> >
>>>> > The repo says, same time when I posted
>>>> > the link first time:
>>>> >
>>>> >> This repository was archived by the
>>>> >> owner on Jul 9, 2026. It is now read-only.
>>>> >
>>>> > Now a USENET user, who had already entitled
>>>> > himself for a couple of irrational accusations
>>>> >
>>>> > towards my side, is asking this question:
>>>> >
>>>> > Chris M. Thomasson schrieb, Jul 24, 2026
>>>> >> Show an outline of what you
>>>> >> need you compute shader to do?
>>>> >
>>>> > Bravo, thats a delay of a wooping 15 days.
>>>> >
>>>> > Bye
>>>>
>>>> Mild Shock schrieb:
>>>>> Hi,
>>>>>
>>>>> Remember when first all local AI was Python
>>>>> and PyTorch APIs. And then suddently people started
>>>>> using bare metal C/C++ Code. Here is the story:
>>>>>
>>>>> How it started:
>>>>>
>>>>> GPT-J or GPT-J-6B is an open-source large
>>>>> language model (LLM) developed by EleutherAI
>>>>> in 2021. As the name suggests, it is a
>>>>> generative pre-trained transformer model
>>>>> designed to produce human-like text that
>>>>> continues from a prompt.
>>>>> https://www.eleuther.ai/
>>>>>
>>>>> How it was going [Georgi Gerganov]:
>>>>>
>>>>> So a few days later comes out the LLaMA, I do
>>>>> some calculations and I figure out “Okay, 65
>>>>> billion parameters. You probably need about
>>>>> 40 gigs of RAM, with 4-bit quantization. So
>>>>> this can run on a MacBook. Why not do it?”
>>>>>
>>>>> Why I was able to do it so quickly - basically,
>>>>> for all that I saw it’s pretty much GPT-J architecture
>>>>> with some modifications, like some extra memorization
>>>>> layers. It’s minor changes. Basically, again, the
>>>>> existing code for the GPT-J, I just simply
>>>>> modified it there, it happened pretty quickly.
>>>>> https://changelog.com/podcast/532
>>>>>
>>>>> Georgi Gerganov, Bulgarian, now with Hugging
>>>>> Face, ggml-cann also running on Chinese AI chips.
>>>>> ggml Manifesto https://github.com/ggml-org/ggml
>>>>>
>>>>> Bye
>>>>
>>>
>>
>
Back to sci.logic | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
The Wuhan Virus that destroyed Python [ggml Manifesto] Mild Shock <janburse@fastmail.fm> - 2026-07-22 21:01 +0200
Deadlock Exorcism: Switch from Push to Pull [A pi-calculus Specification of Prolog] (Re: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-07-23 00:25 +0200
Why do you even need a mpmc queue? [Thunder Kittens] (Re: Deadlock Exorcism: Switch from Push to Pull) Mild Shock <janburse@fastmail.fm> - 2026-07-23 08:45 +0200
Trivial balancing example for (int i=0; i<global_id; i++) (Re: Why do you even need a mpmc queue? [Thunder Kittens]) Mild Shock <janburse@fastmail.fm> - 2026-07-23 08:55 +0200
The Pixel Phone AI Experiment Song (Enqueue/dequeue need not be fast and can spinn ["fairness" questions]) Mild Shock <janburse@fastmail.fm> - 2026-07-23 09:19 +0200
Enqueue/dequeue need not be fast and can spinn ["fairness" questions] (Re: The Pixel Phone AI Experiment Song (Enqueue/dequeue need not be fast and can spinn ["fairness" questions]) Mild Shock <janburse@fastmail.fm> - 2026-07-23 09:23 +0200
And, where did I talk about rockets? [Hint its about xAI's Grok] (Re: Why do you even need a mpmc queue? [Thunder Kittens]) Mild Shock <janburse@fastmail.fm> - 2026-07-25 01:25 +0200
Why forget something, that was never on my mind (Re: And, where did I talk about rockets? [Hint its about xAI's Grok]) Mild Shock <janburse@fastmail.fm> - 2026-07-25 09:49 +0200
Example Mandel Brot rendering [Faster with MIMD] (Was: Why do you even need a mpmc queue? [Thunder Kittens]) Mild Shock <janburse@fastmail.fm> - 2026-07-25 09:56 +0200
Potential Python Recovery: Free Threading [3.13 release] (Re: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-07-23 10:21 +0200
The things XILINX braught to the AMD table (Re: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-07-23 18:48 +0200
NVIDIA evacuated its Chinese market [Tau Scaling] (Re: The things XILINX braught to the AMD table) Mild Shock <janburse@fastmail.fm> - 2026-07-23 19:13 +0200
Micro penis mother sung arias (Re: NVIDIA evacuated its Chinese market [Tau Scaling]) Mild Shock <janburse@fastmail.fm> - 2026-07-24 14:40 +0200
Micro penis brain is in constant hiatus (Re: Micro penis mother sung arias) Mild Shock <janburse@fastmail.fm> - 2026-07-24 15:27 +0200
Ignoramus or Ignorabimus: I don't care [(Re: Micro penis brain is in constant hiatus (Re: Micro penis mother sung arias) Mild Shock <janburse@fastmail.fm> - 2026-07-24 15:35 +0200
You are a moron, brainless putin payed (Re: Ignoramus or Ignorabimus: I don't care) Mild Shock <janburse@fastmail.fm> - 2026-07-24 18:01 +0200
Yeah keep reading my posts, uninspired fool (Re: You are a moron, brainless putin payed) Mild Shock <janburse@fastmail.fm> - 2026-07-24 19:47 +0200
Out of the blue accusation span 15 days [Empirical USENET study] (Re: Ignoramus or Ignorabimus: I don't care) Mild Shock <janburse@fastmail.fm> - 2026-07-24 20:27 +0200
A brain desease of 20 days [Rossy Boy] (Re: Ignoramus or Ignorabimus: I don't care) Mild Shock <janburse@fastmail.fm> - 2026-07-29 18:41 +0200
I didn't use a Ryzen Halo, whats wrong with you? (Re: A brain desease of 20 days [Rossy Boy]) Mild Shock <janburse@fastmail.fm> - 2026-07-29 23:25 +0200
Ignoramus / Ignorabimus Barometer: Almost 1 Month (Re: A brain desease of 20 days [Rossy Boy]) Mild Shock <janburse@fastmail.fm> - 2026-08-03 00:07 +0200
Food for thought: Bayesian Experimental Designer (Re: A brain desease of 20 days [Rossy Boy]) Mild Shock <janburse@fastmail.fm> - 2026-09-24 15:43 +0200
Re: Food for thought: Bayesian Experimental Designer (Re: A brain desease of 20 days [Rossy Boy]) Mild Shock <janburse@fastmail.fm> - 2026-09-24 15:44 +0200
What will microsoft say, will they buy it? (Was: Food for thought: Bayesian Experimental Designer) Mild Shock <janburse@fastmail.fm> - 2026-09-24 15:46 +0200
Re: NVIDIA evacuated its Chinese market [Tau Scaling] (Re: The things XILINX braught to the AMD table) Mild Shock <janburse@fastmail.fm> - 2026-07-28 14:17 +0200
ASML stocks are plunging, bye bye dutchies (Re: NVIDIA evacuated its Chinese market [Tau Scaling]) Mild Shock <janburse@fastmail.fm> - 2026-07-28 14:18 +0200
Little Data Center on Your Palm [AI Laptops for 500 USD] (Re: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-07-24 17:59 +0200
2008: 4 Blades + Tesla S1070 versus 2026: 1 AI Laptop (Re: Little Data Center on Your Palm [AI Laptops for 500 USD]) Mild Shock <janburse@fastmail.fm> - 2026-07-24 18:15 +0200
Budget AI Laptop 2026 versus Cray T3D 1995 (Was: Little Data Center on Your Palm) Mild Shock <janburse@fastmail.fm> - 2026-08-05 14:21 +0200
Re: Budget AI Laptop 2026 versus Cray T3D 1995 R Kym Horsell <kym@sdf.org> - 2026-08-05 21:11 +0000
AI Alarmist with Supercomputer on Yacht [Horsy Boy] (Was: Budget AI Laptop 2026 versus Cray T3D 1995) Mild Shock <janburse@fastmail.fm> - 2026-08-06 13:21 +0200
Re: AI Alarmist with Supercomputer on Yacht [Horsy Boy] R Kym Horsell <kym@sdf.org> - 2026-08-06 11:56 +0000
Warning: Inconsistencies can summon Waluigis Mild Shock <janburse@fastmail.fm> - 2026-09-14 11:51 +0200
Hurry the blue bus doesnt stop indefinitely (Re: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-07-24 20:37 +0200
Not SIMD, a MIMD design for NVIDIA Volta (Re: Hurry the blue bus doesnt stop indefinitely) Mild Shock <janburse@fastmail.fm> - 2026-07-24 20:58 +0200
Could take 3-4 months find machine / browser (Re: Not SIMD, a MIMD design for NVIDIA Volta) Mild Shock <janburse@fastmail.fm> - 2026-07-24 21:16 +0200
The Koan of pi-WAM queues [FORTRAN-S] (Re: Not SIMD, a MIMD design for NVIDIA Volta) Mild Shock <janburse@fastmail.fm> - 2026-07-26 19:54 +0200
The turbo capping of AI Laptops (Was: The Koan of pi-WAM queues [FORTRAN-S]) Mild Shock <janburse@fastmail.fm> - 2026-07-26 20:00 +0200
Re: The Koan of pi-WAM queues [FORTRAN-S] (Re: Not SIMD, a MIMD design for NVIDIA Volta) Mild Shock <janburse@fastmail.fm> - 2026-07-27 09:16 +0200
Why forget Bulgarians, never on my mind (Re: The Koan of pi-WAM queues [FORTRAN-S]) Mild Shock <janburse@fastmail.fm> - 2026-07-27 09:16 +0200
miniTriton CUDA is an alternative to torch variants (Re: Why forget Bulgarians, never on my mind) Mild Shock <janburse@fastmail.fm> - 2026-07-27 09:52 +0200
Andrej Karpathy original gangster of Budget Laptop (Re: miniTriton CUDA is an alternative to torch variants) Mild Shock <janburse@fastmail.fm> - 2026-07-27 09:54 +0200
The evolution of hardware and GPT-2 training (Re: Why forget Bulgarians, never on my mind) Mild Shock <janburse@fastmail.fm> - 2026-07-27 10:57 +0200
How speed up π-WAM with vector operations (Re: The evolution of hardware and GPT-2 training) Mild Shock <janburse@fastmail.fm> - 2026-07-27 11:10 +0200
AI accelerator extend from GPU to CPU [Zero Copying] (Re: How speed up π-WAM with vector operations) Mild Shock <janburse@fastmail.fm> - 2026-07-27 13:21 +0200
The invention of vector and matrix registers [NVIDIA Volta] (Re: AI accelerator extend from GPU to CPU [Zero Copying]) Mild Shock <janburse@fastmail.fm> - 2026-07-27 13:22 +0200
Re: The invention of vector and matrix registers [NVIDIA Volta] (Re: AI accelerator extend from GPU to CPU [Zero Copying]) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-27 07:34 -0700
Maybe they should have named it NVIDIA Einstein [Rossy Boy Toe Sucking] (Was: The invention of vector and matrix registers [NVIDIA Volta]) Mild Shock <janburse@fastmail.fm> - 2026-07-27 17:12 +0200
Re: The invention of vector and matrix registers [NVIDIA Volta] (Re: AI accelerator extend from GPU to CPU [Zero Copying]) R Kym Horsell <kym@sdf.com> - 2026-07-27 15:43 +0000
Re: The invention of vector and matrix registers [NVIDIA Volta] (Re: AI accelerator extend from GPU to CPU [Zero Copying]) R Kym Horsell <kymhorsell@gmail.com> - 2026-07-27 15:46 +0000
π-WAM is not adding decimals, it is removing decimals (Was: The invention of vector and matrix registers [NVIDIA Volta]) Mild Shock <janburse@fastmail.fm> - 2026-07-27 18:34 +0200
In Budget Laptops the TOPS come with low energy footprint (Re: π-WAM is not adding decimals, it is removing decimals) Mild Shock <janburse@fastmail.fm> - 2026-07-27 18:45 +0200
Potato Computer owner impressed by Ukraine Tech [Rossy Boys Brother?] (Was: Hurry the blue bus doesnt stop indefinitely) Mild Shock <janburse@fastmail.fm> - 2026-07-27 16:56 +0200
Rossy Boy is neither Einstein nor Zweistein (Was: Potato Computer owner impressed by Ukraine Tech) Mild Shock <janburse@fastmail.fm> - 2026-07-27 18:25 +0200
You are still chewing on SIMD. LoL (Re: Rossy Boy is neither Einstein nor Zweistein) Mild Shock <janburse@fastmail.fm> - 2026-07-29 17:12 +0200
Hurry Rossy Boy, the blue bus is waiting (Re: You are still chewing on SIMD. LoL) Mild Shock <janburse@fastmail.fm> - 2026-07-29 17:53 +0200
Look how they advertized CUDA and logical threads (Re: Hurry Rossy Boy, the blue bus is waiting) Mild Shock <janburse@fastmail.fm> - 2026-07-29 17:55 +0200
Forget any arithmetization of product FSA (Re: Look how they advertized CUDA and logical threads) Mild Shock <janburse@fastmail.fm> - 2026-07-29 17:58 +0200
Rossy Boys tears could cool a data center [pi-WAM Interleaved Synchronized Emulator] (Re: You are still chewing on SIMD. LoL) Mild Shock <janburse@fastmail.fm> - 2026-07-29 20:06 +0200
I don't use Rust, you are crazy [Jump off a bridge, idiot] (Re: Rossy Boys tears could cool a data center [pi-WAM Interleaved Synchronized Emulator]) Mild Shock <janburse@fastmail.fm> - 2026-07-29 20:25 +0200
Hack ecosystem ignorance paired with paranoia [Nand to Tetris] (Re: I don't use Rust, you are crazy) Mild Shock <janburse@fastmail.fm> - 2026-07-29 22:52 +0200
A funny Q16.16 experiment with Hack (Re: Hack ecosystem ignorance paired with paranoia [Nand to Tetris]) Mild Shock <janburse@fastmail.fm> - 2026-07-29 23:11 +0200
Summer Challenge: libSQL = Prolog+Modes [VDBE versus π-WAM] (Was: A funny Q16.16 experiment with Hack) Mild Shock <janburse@fastmail.fm> - 2026-07-30 11:25 +0200
I wrote Hack VM for π-WAM from scratch [4 Months total JavaScript, Python and Java] (Re: Hack ecosystem ignorance paired with paranoia) Mild Shock <janburse@fastmail.fm> - 2026-07-30 19:37 +0200
For WebGPU I first had SIMD in mind (Re: I wrote Hack VM for π-WAM from scratch) Mild Shock <janburse@fastmail.fm> - 2026-07-30 19:51 +0200
Corr.: 4 Months --> 4 Weeks (Re: For WebGPU I first had SIMD in mind) Mild Shock <janburse@fastmail.fm> - 2026-07-30 20:05 +0200
MIPS is a big Huffman mess [But Hack could do it] (Re: I wrote Hack VM for π-WAM from scratch) Mild Shock <janburse@fastmail.fm> - 2026-07-30 22:32 +0200
Not declarative with PHI (Φ) nodes (Was: MIPS is a big Huffman mess [But Hack could do it]) Mild Shock <janburse@fastmail.fm> - 2026-07-30 22:38 +0200
Not declarative with PHI (Φ) nodes (Re: MIPS is a big Huffman mess [But Hack could do it]) Mild Shock <janburse@fastmail.fm> - 2026-07-30 22:39 +0200
Re: MIPS is a big Huffman mess [But Hack could do it] (Re: I wrote Hack VM for π-WAM from scratch) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-31 09:52 -0700
Re: MIPS is a big Huffman mess [But Hack could do it] (Re: I wrote Hack VM for π-WAM from scratch) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-31 10:00 -0700
Re: MIPS is a big Huffman mess [But Hack could do it] (Re: I wrote Hack VM for π-WAM from scratch) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-31 10:07 -0700
Quo Vadis: Extend investigations to WebNN (Was: I wrote Hack VM for π-WAM from scratch [4 Months total JavaScript, Python and Java]) Mild Shock <janburse@fastmail.fm> - 2026-07-31 20:43 +0200
Standing on the shoulders of giants (Re: I don't use Rust, you are crazy [Jump off a bridge, idiot]) Mild Shock <janburse@fastmail.fm> - 2026-08-04 03:19 +0200
You Thief! Stealing Szemeredi, Aristotle, Leibniz, etc.. (Re: Standing on the shoulders of giants) Mild Shock <janburse@fastmail.fm> - 2026-08-04 15:19 +0200
How Rossy Boys plagiarism works [Copy Paste Slop] (Re: You Thief! Stealing Szemeredi, Aristotle, Leibniz, etc.. ) Mild Shock <janburse@fastmail.fm> - 2026-08-04 17:58 +0200
Statistics gave up, no salient truth [Signal Collapse] Re: How Rossy Boys plagiarism works [Copy Paste Slop] (Re: You Thief! Stealing Szemeredi, Aristotle, Leibniz, etc.. ) Mild Shock <janburse@fastmail.fm> - 2026-08-04 18:17 +0200
Is Bill Gates right that we will loose jobs [Talkie x Claw] (Re: Rossy Boys tears could cool a data center) Mild Shock <janburse@fastmail.fm> - 2026-09-03 23:39 +0200
The Flagging of Students for not Thinking [Elixir Evolution] (Was: Is Bill Gates right that we will loose jobs [Talkie x Claw]) Mild Shock <janburse@fastmail.fm> - 2026-09-04 11:45 +0200
Rust Eggs for Statechart Proof Certificates? (Was: The Flagging of Students for not Thinking [Elixir Evolution]) Mild Shock <janburse@fastmail.fm> - 2026-09-05 14:17 +0200
Axiom of Determinacy as SCXML × SCXML [AI Chatbot Help] (Re: Rust Eggs for Statechart Proof Certificates? (Was: The Flagging of Students for not Thinking [Elixir Evolution])) Mild Shock <janburse@fastmail.fm> - 2026-09-05 16:11 +0200
The Paul Armer Square Revisited (Was: "Mathematics in the Age of AI") Mild Shock <janburse@fastmail.fm> - 2026-08-19 23:49 +0200
Communism will Save Us! [Pivot Russia for China] (Re: The Paul Armer Square Revisited) Mild Shock <janburse@fastmail.fm> - 2026-08-20 13:15 +0200
How to increase your "Convincingness" [Anthropic AI Text Hacked] Mild Shock <janburse@fastmail.fm> - 2026-08-20 19:31 +0200
Free Speech for (my) Robots [Kristallnaach BAP] (Re: How to increase your "Convincingness") Mild Shock <janburse@fastmail.fm> - 2026-08-20 19:49 +0200
Reality of Proof Assistants / Coding [Luhmanns Zettelkasten] (Re: Free Speech for (my) Robots) Mild Shock <janburse@fastmail.fm> - 2026-08-20 20:23 +0200
The Bazar is dead, long live the Bazar [Swarm AI] (Was: Hurry the blue bus doesnt stop indefinitely) Mild Shock <janburse@fastmail.fm> - 2026-09-21 11:25 +0200
New! P(tao) versus the Euler Turbine [Navier Stokes] (Was: The Bazar is dead, long live the Bazar) Mild Shock <janburse@fastmail.fm> - 2026-09-22 08:38 +0200
Tristan Buckmaster was too quick? [Navier Stockes OpenAI] (Was: New! P(tao) versus the Euler Turbine) Mild Shock <janburse@fastmail.fm> - 2026-10-13 23:19 +0200
Lean versus Natural Language (Re: Tristan Buckmaster was too quick? [Navier Stockes OpenAI] (Was: New! P(tao) versus the Euler Turbine)) Mild Shock <janburse@fastmail.fm> - 2026-10-13 23:37 +0200
ean 4: Basically just Microsoft Advertising (Was: Lean versus Natural Language) Mild Shock <janburse@fastmail.fm> - 2026-10-15 11:27 +0200
Lean 4: Basically just Microsoft Advertising Re: Lean versus Natural Language (Re: Tristan Buckmaster was too quick? [Navier Stockes OpenAI] (Was: New! P(tao) versus the Euler Turbine)) Mild Shock <janburse@fastmail.fm> - 2026-10-15 11:27 +0200
Got it. Or are you too stupid? [New Usenet Mantra] (Was: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-07-27 18:59 +0200
Lamas in a cradle and Lamas on the edge [Red Pyjama] (Re: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-07-29 13:03 +0200
AI Accelerators and ISO Prolog multi-threading (Re: Lamas in a cradle and Lamas on the edge [Red Pyjama]) Mild Shock <janburse@fastmail.fm> - 2026-07-29 17:02 +0200
Actor/Erlang is dead, no Thread and Mailbox conflation [golang channels] (Re: AI Accelerators and ISO Prolog multi-threading) (Re: Lamas in a cradle and Lamas on the edge [Red Pyjama]) Mild Shock <janburse@fastmail.fm> - 2026-07-29 17:04 +0200
Can library(ironpaw) repurpose FFT hardware [Glimps into Ryzen AI 7 350] (Re: Actor/Erlang is dead, no Thread and Mailbox conflation ) Mild Shock <janburse@fastmail.fm> - 2026-08-01 02:32 +0200
Tablet and phone UBS-C remote debugging (Re: Lamas in a cradle and Lamas on the edge [Red Pyjama]) Mild Shock <janburse@fastmail.fm> - 2026-08-01 12:19 +0200
NPUs doing 2d chess comms (Manhattan Distance or L1 Norm) (Re: Tablet and phone UBS-C remote debugging) Mild Shock <janburse@fastmail.fm> - 2026-08-01 14:12 +0200
NACK retransmission might double Manhattan Distance (Re: NPUs doing 2d chess comms) Mild Shock <janburse@fastmail.fm> - 2026-08-01 14:24 +0200
I am using WebGPU, and not WebGL (Re: NACK retransmission might double Manhattan Distance) Mild Shock <janburse@fastmail.fm> - 2026-08-02 00:47 +0200
Texture inside my compute shader makes no sense (Re: I am using WebGPU, and not WebGL) Mild Shock <janburse@fastmail.fm> - 2026-08-02 02:40 +0200
Prolog inferencing and not canvasing fancy stuff (Re: Texture inside my compute shader makes no sense) Mild Shock <janburse@fastmail.fm> - 2026-08-02 02:42 +0200
It’s called . . . . enshittification (About the price tag for using a multifile/1) Mild Shock <janburse@fastmail.fm> - 2026-08-14 00:49 +0200
First AI laptops, now AI single-boarders [Budget, Budget, ..] (Was: NPUs doing 2d chess comms (Manhattan Distance or L1 Norm)) Mild Shock <janburse@fastmail.fm> - 2026-08-26 00:07 +0200
Food for thought: ISOMICRO profile of Web Prolog (Was: First AI laptops, now AI single-boarders [Budget, Budget, ..]) Mild Shock <janburse@fastmail.fm> - 2026-08-31 18:02 +0200
Food for thought: Le Petit Bistro as a Trinity Use Case (Was: Food for thought: ISOMICRO profile of Web Prolog) Mild Shock <janburse@fastmail.fm> - 2026-09-02 21:51 +0200
Giga Lips for Prolog based Chatting (Re: Food for thought: Le Petit Bistro as a Trinity Use Case) Mild Shock <janburse@fastmail.fm> - 2026-09-02 21:55 +0200
Google holds the keys to the AI kingdom [WebClaw Dominance] (Was: Giga Lips for Prolog based Chatting) Mild Shock <janburse@fastmail.fm> - 2026-09-03 09:42 +0200
Chris M. Thomasson can ask 100 more questions (Was: Tablet and phone UBS-C remote debugging) Mild Shock <janburse@fastmail.fm> - 2026-08-02 02:46 +0200
npm install webgpu [Google Dawn] (Re: Chris M. Thomasson can ask 100 more questions) Mild Shock <janburse@fastmail.fm> - 2026-08-02 03:03 +0200
GPU elasticity was already invented in 2008 with CUDA (Re: npm install webgpu [Google Dawn]) Mild Shock <janburse@fastmail.fm> - 2026-08-03 00:01 +0200
Synthetic Multilanguage Autoformalization Dataset [Informath project] (Was: Lamas in a cradle and Lamas on the edge [Red Pyjama]) Mild Shock <janburse@fastmail.fm> - 2026-08-08 09:17 +0200
Re: Synthetic Multilanguage Autoformalization Dataset [Informath project] (Was: Lamas in a cradle and Lamas on the edge [Red Pyjama]) x3 <x@x.net> - 2026-08-08 11:45 -0700
Nice try Rossy Boy --> **plonk** (Was: Synthetic Multilanguage Autoformalization Dataset [Informath project]) Mild Shock <janburse@fastmail.fm> - 2026-08-08 23:02 +0200
Ethernal September Idiots Gone (Was: Nice try Rossy Boy --> **plonk**) Mild Shock <janburse@fastmail.fm> - 2026-08-08 23:15 +0200
Six Proofs and Generally Inteligent Systems [EyeProlog Pseudo Scientism] (Re: Synthetic Multilanguage Autoformalization Dataset [Informath project]) Mild Shock <janburse@fastmail.fm> - 2026-08-15 15:19 +0200
Everybody does eat and sleep [The SK hynix Story] (Was: Six Proofs and Generally Intelligent Systems [EyeProlog Pseudo Scientism]) Mild Shock <janburse@fastmail.fm> - 2026-08-15 18:47 +0200
Even send_color and recv_color can block [Cerebras Waver] (Re: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-08-02 23:39 +0200
GPU Elasticity: Collective Communications Libraries (Re: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-08-07 14:35 +0200
What are Flits and Phits? [Network on a Chip] (Was: GPU Elasticity: Collective Communications Libraries) Mild Shock <janburse@fastmail.fm> - 2026-08-07 18:05 +0200
The Mac Neo is a Budget Monster [GPU Channels] (Re: What are Flits and Phits? [Network on a Chip]) Mild Shock <janburse@fastmail.fm> - 2026-08-11 16:25 +0200
The luminaries of duct-tape engineering [Sweeney and Torvald] (Re: The Mac Neo is a Budget Monster [GPU Channels]) Mild Shock <janburse@fastmail.fm> - 2026-08-11 16:54 +0200
Cristallina: Thank you for the Beam (Was: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-08-09 21:19 +0200
Re: Cristallina: Thank you for the Beam (Was: The Wuhan Virus that destroyed Python [ggml Manifesto]) Mild Shock <janburse@fastmail.fm> - 2026-08-18 14:56 +0200
Giant Shoulders for AI Surprises (Was: Cristallina: Thank you for the Beam) Mild Shock <janburse@fastmail.fm> - 2026-08-18 14:57 +0200
Loderunner Enemy AI better than SWI-Prolog? [Prolog Education Group] Mild Shock <janburse@fastmail.fm> - 2026-08-18 16:23 +0200
How to shoot yourself in the foot (Was: Loderunner Enemy AI better than SWI-Prolog? [Prolog Education Group]) Mild Shock <janburse@fastmail.fm> - 2026-08-18 16:42 +0200
William A. Howard solved all his 99 problems (Re: Loderunner Enemy AI better than SWI-Prolog?) Mild Shock <janburse@fastmail.fm> - 2026-08-23 01:47 +0200
Mojo: The Small Hands Paradox [Maastrichtian Stage] (Was: The Wuhan Virus that destroyed Python) Mild Shock <janburse@fastmail.fm> - 2026-09-15 14:31 +0200
More from the Trailer Park Boys (Re: Mojo: The Small Hands Paradox [Maastrichtian Stage]) Mild Shock <janburse@fastmail.fm> - 2026-09-15 19:41 +0200
Interdisplinary Research for kill -9 (SIGKILL) (Was: More from the Trailer Park Boys) Mild Shock <janburse@fastmail.fm> - 2026-09-16 13:23 +0200
Kundalini III: Modus Barbara versus Stock Pumping (Re: Interdisplinary Research for kill -9 (SIGKILL)) Mild Shock <janburse@fastmail.fm> - 2026-09-19 13:17 +0200
Mathematical cheese versus "intuition" (Re: Kundalini III: Modus Barbara versus Stock Pumping) Mild Shock <janburse@fastmail.fm> - 2026-09-22 10:23 +0200
Re: Mathematical cheese versus "intuition" (Re: Kundalini III: Modus Barbara versus Stock Pumping) Mild Shock <janburse@fastmail.fm> - 2026-09-22 16:09 +0200
A real Terence Tao Ingestion Problem (Was: Mathematical cheese versus "intuition") Mild Shock <janburse@fastmail.fm> - 2026-09-22 16:10 +0200
The A2A project: Agent cards for collaboration) Mild Shock <janburse@fastmail.fm> - 2026-09-22 16:30 +0200
Self censoring of not talking "superintelligence" (Was: Mojo: The Small Hands Paradox [Maastrichtian Stage]) Mild Shock <janburse@fastmail.fm> - 2026-09-22 18:00 +0200
The Ben Goertzel talkie genes (Was: Re: Self censoring of not talking "superintelligence") Mild Shock <janburse@fastmail.fm> - 2026-09-22 18:06 +0200
Philosophy Departments lead in GenAI Adoption? (Was: The Ben Goertzel talkie genes) Mild Shock <janburse@fastmail.fm> - 2026-09-22 20:11 +0200
csiph-web