Hi,
Why is nobody mentioning Agda here. It has
beautiful dependent types, and tactics are
just programs. Poor Henk Barendregt, not
everybody likes dependent types it seems:
Are we stuck with Lean?
https://mathoverflow.net/q/513742/
Does Depependent types require proof objects,
which waste large amounts of memory. Well,
if you are not good in erasing them.
But is there a Red Pyjama for Proof Assistants,
the baby cradle where LLMs can learn proof
assistant lingua and strategies. It seems
yes, synthetic data corpuses to the rescue:
We address this gap by introducing SMAD
(Synthetic Multilanguage Autoformalization
Dataset), a 400K 4-to-3 parallel corpus
covering four formal languages (Dedukti,
Agda, Coq, Lean) and three natural languages (
English, French, Swedish), generated via
the Informath project.
https://github.com/GrammaticalFramework/informath
But the corpus could be an accident, maybe rather
a toy from the https://www.grammaticalframework.org/
folks, will this have an impact?
Bye
Mild Shock schrieb:
Hi,
Why does this Lama have a red pyjama.
Oh, its a baby Lama. Its still in the cradle
and needs some training:
RedPajama-Data-v2
https://github.com/togethercomputer/RedPajama-Data
But then Andrej Karpathy recently showed
GPT-2 training on rented GPUs for less
than 100 USD in less then 2 hours.
So where do these grown up Lamas go.
Well Georgi Gerganov prefered C++/C
when he shouted Llama Llama Red Pyjama.
But you also find WebLLM, wrapping the
underlying C++/C GPU interface via the
W3C standard WebGPU / WGSL, with JavaScript:
In-Browser LLM Inference Engine
https://webllm.mlc.ai/
My experience with WebLLM 6 months
ago on an iPad Pro 2024, still a little early
stage performance and robustness.
But hey hardware of AI mobile iGPUs is
still evolving, and AI laptop, AI smartphones
and AI tablets, will soon feature Chinese
hardware such some new Kirin AI in 2027.
Bye
Mild Shock schrieb:
Hi,
Maybe there is a Rossy Boy flux generator
web server with infinity and continuity
HTTPS and .mjs type, aka SIMT halucination.
To run the GPU example that is written in HTML,
JavaScript and WebGPU / WGSL, the minium is
possibly a HTTPS server that can deliver the
right mime type for the .mjs extension. Its
then only a bundle of static pages that does
the demonstration. What worked on my side
is the IntelliJ browse button, which then uses
a small local server on its own, sandboxed to
serving some project files.
But this is only how to launch the test pages.
The Rossy Boy SIMT halucination, could also work, who knows?
Bye
Mild Shock schrieb:
Hi,
Nobody cares about CivetWeb a C++/C library,
the rossy boy moron refuses to understand this
simple GPU test, that shows some AI Acceleration:
11.4 Giga Lips with a Budget Laptop
https://github.com/Jean-Luc-Picard-2021/gigabudget
Bye
Johann 'Myrkraverk' Oskarsson schrieb:
On 29/07/2026 5:15 PM, Mild Shock wrote:
Hi,
Confused rossy boy is confused. We are
not building a stupid web server, where
a listener thread spawns service threads,
and to avoid malloc and free, reuses
a pool, or some shitty fork join framework.
The producer and consumer example I posted
elsewhere archived a dataflow without
malloc and free of threads. You are miles
away from what we are doing here.
Why not?˙ Isn't this comp.lang.c?˙ And isn't that exactly how
CivetWeb works internally?˙ Have you never built your own web
sever in C?˙ Not even with CivetWeb?˙ It's really easy!˙ You
only need to implement a callback or two.
Hi,
Years ago Sam Altman said to have no idea how
to generate revenue, but when the generally
intelligent system is in place, he might ask it.
Some schools approach the ?generality? from
a totally wrong perspective. Take the EyeProlog
Pseudo Scientism here:
The Art of EyeProlog https://eyereasoner.github.io/eyeprolog/the-art-of-eyeprolog
It is the same nonsense like constraint propagation,
the idea here is to evolve better software, that it
has as a main component refinement:
Start -> Algo1 -> Algo2 -> Algo3 -> Algo4 ...
But EyeProlog itself is an example of not using
this refinement. Like dropping the classical
WAM architecture, and back to YieldProlog somehow.
What if the world ticks like this
when it come to generality:
˙˙˙˙˙˙ /-> Algo1
˙˙˙˙˙ /--> Algo2
Start ---> Algo3
˙˙˙˙˙ \--> Algo4
˙˙˙˙˙˙ \-> ...
Innovation requires to start from scratch.
I think this little booklet, recommended by
Ernst Specker, Proofs from THE BOOK is a
book of mathematical proofs by Martin Aigner
and Gnter M. Ziegler, first published in 1998.
Just wants to teach us about this bifurcation:
Chapter 1: Six proofs of the infinity of
the primes, including Euclid's and Furstenberg's. https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK
Yeah, lets aim for surprises by
generative AI, not refinement.
Bye
See also:
Sam Altman on his Business Model
https://www.youtube.com/shorts/pLnyjxgFxew
Mild Shock schrieb:
Hi,
Why is nobody mentioning Agda here. It has
beautiful dependent types, and tactics are
just programs. Poor Henk Barendregt, not
everybody likes dependent types it seems:
Are we stuck with Lean?
https://mathoverflow.net/q/513742/
Does Depependent types require proof objects,
which waste large amounts of memory. Well,
if you are not good in erasing them.
But is there a Red Pyjama for Proof Assistants,
the baby cradle where LLMs can learn proof
assistant lingua and strategies. It seems
yes, synthetic data corpuses to the rescue:
We address this gap by introducing SMAD
(Synthetic Multilanguage Autoformalization
Dataset), a 400K 4-to-3 parallel corpus
covering four formal languages (Dedukti,
Agda, Coq, Lean) and three natural languages (
English, French, Swedish), generated via
the Informath project.
https://github.com/GrammaticalFramework/informath
But the corpus could be an accident, maybe rather
a toy from the https://www.grammaticalframework.org/
folks, will this have an impact?
Bye
Mild Shock schrieb:
Hi,
Why does this Lama have a red pyjama.
Oh, its a baby Lama. Its still in the cradle
and needs some training:
RedPajama-Data-v2
https://github.com/togethercomputer/RedPajama-Data
But then Andrej Karpathy recently showed
GPT-2 training on rented GPUs for less
than 100 USD in less then 2 hours.
So where do these grown up Lamas go.
Well Georgi Gerganov prefered C++/C
when he shouted Llama Llama Red Pyjama.
But you also find WebLLM, wrapping the
underlying C++/C GPU interface via the
W3C standard WebGPU / WGSL, with JavaScript:
In-Browser LLM Inference Engine
https://webllm.mlc.ai/
My experience with WebLLM 6 months
ago on an iPad Pro 2024, still a little early
stage performance and robustness.
But hey hardware of AI mobile iGPUs is
still evolving, and AI laptop, AI smartphones
and AI tablets, will soon feature Chinese
hardware such some new Kirin AI in 2027.
Bye
Mild Shock schrieb:
Hi,
Maybe there is a Rossy Boy flux generator
web server with infinity and continuity
HTTPS and .mjs type, aka SIMT halucination.
To run the GPU example that is written in HTML,
JavaScript and WebGPU / WGSL, the minium is
possibly a HTTPS server that can deliver the
right mime type for the .mjs extension. Its
then only a bundle of static pages that does
the demonstration. What worked on my side
is the IntelliJ browse button, which then uses
a small local server on its own, sandboxed to
serving some project files.
But this is only how to launch the test pages.
The Rossy Boy SIMT halucination, could also work, who knows?
Bye
Mild Shock schrieb:
Hi,
Nobody cares about CivetWeb a C++/C library,
the rossy boy moron refuses to understand this
simple GPU test, that shows some AI Acceleration:
11.4 Giga Lips with a Budget Laptop
https://github.com/Jean-Luc-Picard-2021/gigabudget
Bye
Johann 'Myrkraverk' Oskarsson schrieb:
On 29/07/2026 5:15 PM, Mild Shock wrote:
Hi,
Confused rossy boy is confused. We are
not building a stupid web server, where
a listener thread spawns service threads,
and to avoid malloc and free, reuses
a pool, or some shitty fork join framework.
The producer and consumer example I posted
elsewhere archived a dataflow without
malloc and free of threads. You are miles
away from what we are doing here.
Why not?˙ Isn't this comp.lang.c?˙ And isn't that exactly how
CivetWeb works internally?˙ Have you never built your own web
sever in C?˙ Not even with CivetWeb?˙ It's really easy!˙ You
only need to implement a callback or two.
In "Mathematics in the Age OF AI" (2026-08-17) macht Terence
Tao sich auf zirka 11 Seiten Gedanke darber, in welcher Form
KI-Systeme von ihnen gefundene Erkenntnisse bereitstellen und
wie diese in das mathematische Wissen integriert werden sollten.
Hi,
I even don't remember exactly why I landed
in comp.theory. A yes, because Rossy Boy,
was hooked on SIMD and didn't understand Hack.
But the Hack work, rather belongs to my
Alma Mater Zurich and my personal heros, Gutnecht
and Wirth, who wrote a one pass Modula
compiler during some christmas holidays,
back then when I was student. Not sure
whether the Ljubljana School can do that,
when I read this here:
Finite Algebraic Effects as dicts and such https://www.philipzucker.com/bdd_term_alg_effects/
I only find gibberish like:
- ?Data? is somehow less mysterious to me
˙ than ?computation?.˙ [..] I don?t even
˙ know what ?computation? really is
- In temporal logic, there is a logic CTL
˙ which talks about computation trees.
- Algerbaic (LoL) effects is almost a complete
˙ hackery abuse of the notion of arity
˙ and that?s neat.
- Then there are 10^10 etc vectors which
˙ show up if you discretize 3d/4d space. [..]
˙ or reinforcement learning.
- Etc..
WTF is this guy smoking? I mean he even
doesn't uses math notation, only posts
Python code fragments go go,
possibly a Python brain damage.
But still less sever than Rossy Boys.
Bye
Ross Finlayson schrieb:
Hello, here I'll post some design notes and a panel discussion with some
chat-bots about making some sense of the "vector-wide scalar word"
and "character machines", on commodity hardware about ubiquitous
operations.
It's considered at least tangentially relevant to comp.lang.c and
comp.lang.c++ because for example text is ubiquitous and the targets
would be low-level, while the higher-level languages would have a
same sort of patternry, and for example that libc and cstdlib are
standard, and as with regards to POSIX and Unicode and so on.
Please feel free to excuse or ignore, or comment as freely.
Thanks for reading.
Hi,
How it started:
Speed
^
| * Machine
|˙ (1963)
|
|
|˙˙˙˙˙˙˙˙˙˙˙˙ * Man
+--------------------->
Sophistication
How its going?
Speed
^
| * Machine˙˙ * Machine
|˙ (1963)˙˙˙˙˙˙ (2026)
|
|
|˙˙˙˙˙˙˙˙˙˙˙˙ * Man
+--------------------->
Sophistication
Bye
ATTITUDES TOWARD INTELLIGENT MACHINES
Paul Armer
RAND Corporation
in
BIONICS SYMPOSIUM 1960
LIVING PROTOTYPES - THE KEY TO NEW TECHNOLOGY https://books.google.ch/books?id=1ZMeAAAAMAAJ&pg=PA13
Stefan Ram schrieb:
˙˙˙ In "Mathematics in the Age OF AI" (2026-08-17) macht Terence
˙˙˙ Tao sich auf zirka 11 Seiten Gedanke darber, in welcher Form
˙˙˙ KI-Systeme von ihnen gefundene Erkenntnisse bereitstellen und
˙˙˙ wie diese in das mathematische Wissen integriert werden sollten.
Mild Shock schrieb:
Hi,
I even don't remember exactly why I landed
in comp.theory. A yes, because Rossy Boy,
was hooked on SIMD and didn't understand Hack.
But the Hack work, rather belongs to my
Alma Mater Zurich and my personal heros, Gutnecht
and Wirth, who wrote a one pass Modula
compiler during some christmas holidays,
back then when I was student. Not sure
whether the Ljubljana School can do that,
when I read this here:
Finite Algebraic Effects as dicts and such
https://www.philipzucker.com/bdd_term_alg_effects/
I only find gibberish like:
- ?Data? is somehow less mysterious to me
˙˙ than ?computation?.˙ [..] I don?t even
˙˙ know what ?computation? really is
- In temporal logic, there is a logic CTL
˙˙ which talks about computation trees.
- Algerbaic (LoL) effects is almost a complete
˙˙ hackery abuse of the notion of arity
˙˙ and that?s neat.
- Then there are 10^10 etc vectors which
˙˙ show up if you discretize 3d/4d space. [..]
˙˙ or reinforcement learning.
- Etc..
WTF is this guy smoking? I mean he even
doesn't uses math notation, only posts
Python code fragments go go,
possibly a Python brain damage.
But still less sever than Rossy Boys.
Bye
Ross Finlayson schrieb:
Hello, here I'll post some design notes and a panel discussion with some >>> chat-bots about making some sense of the "vector-wide scalar word"
and "character machines", on commodity hardware about ubiquitous
operations.
It's considered at least tangentially relevant to comp.lang.c and
comp.lang.c++ because for example text is ubiquitous and the targets
would be low-level, while the higher-level languages would have a
same sort of patternry, and for example that libc and cstdlib are
standard, and as with regards to POSIX and Unicode and so on.
Please feel free to excuse or ignore, or comment as freely.
Thanks for reading.
Es ist schlimm, das man in der modernen Zeit
trotz KI immer noch von dem spricht, was die
Welt anscheinend antreibt: GELD.
Wer Geld hat, hat Macht, kann Wissen einkaufen -
was ist mit den Rest ? Die kleinen haben kein Geld,
Amerika ist pleite und Deutschland hat nun wieder
eine neue Steuer - Kinderfonds, 10 Euro monatlich,
bis 18, angelegt fr den Staat Deutschland.
Hi,
How it started:
Speed
^
| * Machine
|˙ (1963)
|
|
|˙˙˙˙˙˙˙˙˙˙˙˙ * Man
+--------------------->
Sophistication
How its going?
Speed
^
| * Machine˙˙ * Machine
|˙ (1963)˙˙˙˙˙˙ (2026)
|
|
|˙˙˙˙˙˙˙˙˙˙˙˙ * Man
+--------------------->
Sophistication
Bye
ATTITUDES TOWARD INTELLIGENT MACHINES
Paul Armer
RAND Corporation
in
BIONICS SYMPOSIUM 1960
LIVING PROTOTYPES - THE KEY TO NEW TECHNOLOGY https://books.google.ch/books?id=1ZMeAAAAMAAJ&pg=PA13
Stefan Ram schrieb:
˙˙˙ In "Mathematics in the Age OF AI" (2026-08-17) macht Terence
˙˙˙ Tao sich auf zirka 11 Seiten Gedanke darber, in welcher Form
˙˙˙ KI-Systeme von ihnen gefundene Erkenntnisse bereitstellen und
˙˙˙ wie diese in das mathematische Wissen integriert werden sollten.
Mild Shock schrieb:
Hi,
I even don't remember exactly why I landed
in comp.theory. A yes, because Rossy Boy,
was hooked on SIMD and didn't understand Hack.
But the Hack work, rather belongs to my
Alma Mater Zurich and my personal heros, Gutnecht
and Wirth, who wrote a one pass Modula
compiler during some christmas holidays,
back then when I was student. Not sure
whether the Ljubljana School can do that,
when I read this here:
Finite Algebraic Effects as dicts and such
https://www.philipzucker.com/bdd_term_alg_effects/
I only find gibberish like:
- ?Data? is somehow less mysterious to me
˙˙ than ?computation?.˙ [..] I don?t even
˙˙ know what ?computation? really is
- In temporal logic, there is a logic CTL
˙˙ which talks about computation trees.
- Algerbaic (LoL) effects is almost a complete
˙˙ hackery abuse of the notion of arity
˙˙ and that?s neat.
- Then there are 10^10 etc vectors which
˙˙ show up if you discretize 3d/4d space. [..]
˙˙ or reinforcement learning.
- Etc..
WTF is this guy smoking? I mean he even
doesn't uses math notation, only posts
Python code fragments go go,
possibly a Python brain damage.
But still less sever than Rossy Boys.
Bye
Ross Finlayson schrieb:
Hello, here I'll post some design notes and a panel discussion with some >>> chat-bots about making some sense of the "vector-wide scalar word"
and "character machines", on commodity hardware about ubiquitous
operations.
It's considered at least tangentially relevant to comp.lang.c and
comp.lang.c++ because for example text is ubiquitous and the targets
would be low-level, while the higher-level languages would have a
same sort of patternry, and for example that libc and cstdlib are
standard, and as with regards to POSIX and Unicode and so on.
Please feel free to excuse or ignore, or comment as freely.
Thanks for reading.
Somewhat related to AI watermarking is this recent article in the news.
*What does it mean to put a watermark on AI text?* <https://edition.cnn.com/2026/08/20/us/word-of-the-week-ai-watermark-cec>
Which references:
*How Claude's text watermark works*
<https://www.anthropic.com/news/claude-text-watermark>
*How AI text watermarking works*
<https://declaude.org/watermarking/>
Where apparently there is an EU law which requires watermarking...
There's also this referenced, but it's behind a paywall.
*Technology that can detect text written by AI with 99.9% certainty*
Hi,
The Armer paper gets geopolitical in the end
chapters. But today you could pivot russia for
china, and you would get a nice piece of work.
But who is the Chinese Lenin, that allows
even rocks and stones to participate in
the class struggle?
˙"Finally, it is particularly necessary to
emphasize the importance of the work of Lenin
who in elaborating on the ideas of Marx and
Engels, developed a materialistic theory of
consciousness as a reflection of activity.
Attention should also be given to the Lenistic
statement of the fact that non-living matter
may also possess this property of reflection."
- Paul Armer, Page 22
Bye
Jens Kallup schrieb:
Es ist schlimm, das man in der modernen Zeit
trotz KI immer noch von dem spricht, was die
Welt anscheinend antreibt: GELD.
Wer Geld hat, hat Macht, kann Wissen einkaufen -
was ist mit den Rest ? Die kleinen haben kein Geld,
Amerika ist pleite und Deutschland hat nun wieder
eine neue Steuer - Kinderfonds, 10 Euro monatlich,
bis 18, angelegt fr den Staat Deutschland.
Mild Shock schrieb:
Hi,
How it started:
Speed
^
| * Machine
|˙ (1963)
|
|
|˙˙˙˙˙˙˙˙˙˙˙˙ * Man
+--------------------->
Sophistication
How its going?
Speed
^
| * Machine˙˙ * Machine
|˙ (1963)˙˙˙˙˙˙ (2026)
|
|
|˙˙˙˙˙˙˙˙˙˙˙˙ * Man
+--------------------->
Sophistication
Bye
ATTITUDES TOWARD INTELLIGENT MACHINES
Paul Armer
RAND Corporation
in
BIONICS SYMPOSIUM 1960
LIVING PROTOTYPES - THE KEY TO NEW TECHNOLOGY
https://books.google.ch/books?id=1ZMeAAAAMAAJ&pg=PA13
Stefan Ram schrieb:
˙˙˙ In "Mathematics in the Age OF AI" (2026-08-17) macht Terence
˙˙˙ Tao sich auf zirka 11 Seiten Gedanke darber, in welcher Form
˙˙˙ KI-Systeme von ihnen gefundene Erkenntnisse bereitstellen und
˙˙˙ wie diese in das mathematische Wissen integriert werden sollten.
Mild Shock schrieb:
Hi,
I even don't remember exactly why I landed
in comp.theory. A yes, because Rossy Boy,
was hooked on SIMD and didn't understand Hack.
But the Hack work, rather belongs to my
Alma Mater Zurich and my personal heros, Gutnecht
and Wirth, who wrote a one pass Modula
compiler during some christmas holidays,
back then when I was student. Not sure
whether the Ljubljana School can do that,
when I read this here:
Finite Algebraic Effects as dicts and such
https://www.philipzucker.com/bdd_term_alg_effects/
I only find gibberish like:
- ?Data? is somehow less mysterious to me
˙˙ than ?computation?.˙ [..] I don?t even
˙˙ know what ?computation? really is
- In temporal logic, there is a logic CTL
˙˙ which talks about computation trees.
- Algerbaic (LoL) effects is almost a complete
˙˙ hackery abuse of the notion of arity
˙˙ and that?s neat.
- Then there are 10^10 etc vectors which
˙˙ show up if you discretize 3d/4d space. [..]
˙˙ or reinforcement learning.
- Etc..
WTF is this guy smoking? I mean he even
doesn't uses math notation, only posts
Python code fragments go go,
possibly a Python brain damage.
But still less sever than Rossy Boys.
Bye
Ross Finlayson schrieb:
Hello, here I'll post some design notes and a panel discussion with
some
chat-bots about making some sense of the "vector-wide scalar word"
and "character machines", on commodity hardware about ubiquitous
operations.
It's considered at least tangentially relevant to comp.lang.c and
comp.lang.c++ because for example text is ubiquitous and the targets
would be low-level, while the higher-level languages would have a
same sort of patternry, and for example that libc and cstdlib are
standard, and as with regards to POSIX and Unicode and so on.
Please feel free to excuse or ignore, or comment as freely.
Thanks for reading.
Hi,
I even don't remember exactly why I landed
in comp.theory. A yes, because Rossy Boy,
was hooked on SIMD and didn't understand Hack.
But the Hack work, rather belongs to my
Alma Mater Zurich and my personal heros, Gutnecht
and Wirth, who wrote a one pass Modula
compiler during some christmas holidays,
back then when I was student. Not sure
whether the Ljubljana School can do that,
when I read this here:
Finite Algebraic Effects as dicts and such https://www.philipzucker.com/bdd_term_alg_effects/
I only find gibberish like:
- ?Data? is somehow less mysterious to me
˙ than ?computation?.˙ [..] I don?t even
˙ know what ?computation? really is
- In temporal logic, there is a logic CTL
˙ which talks about computation trees.
- Algerbaic (LoL) effects is almost a complete
˙ hackery abuse of the notion of arity
˙ and that?s neat.
- Then there are 10^10 etc vectors which
˙ show up if you discretize 3d/4d space. [..]
˙ or reinforcement learning.
- Etc..
WTF is this guy smoking? I mean he even
doesn't uses math notation, only posts
Python code fragments go go,
possibly a Python brain damage.
But still less sever than Rossy Boys.
Bye
Ross Finlayson schrieb:
Hello, here I'll post some design notes and a panel discussion with some
chat-bots about making some sense of the "vector-wide scalar word"
and "character machines", on commodity hardware about ubiquitous
operations.
It's considered at least tangentially relevant to comp.lang.c and
comp.lang.c++ because for example text is ubiquitous and the targets
would be low-level, while the higher-level languages would have a
same sort of patternry, and for example that libc and cstdlib are
standard, and as with regards to POSIX and Unicode and so on.
Please feel free to excuse or ignore, or comment as freely.
Thanks for reading.
| Sysop: | Tetrazocine |
|---|---|
| Location: | Melbourne, VIC, Australia |
| Users: | 9 |
| Nodes: | 8 (0 / 8) |
| Uptime: | 245:19:57 |
| Calls: | 220 |
| Files: | 21,513 |
| Messages: | 83,772 |