Every does eat and sleep. Thats not,
don't give up and restart:
Cite 100 collegues, cite 100 papers, and
do 100 Python snippets. Thats only warm-up!
About - Hi, I’m Philip Zucker!
https://www.philipzucker.com/about/
One the other hand, that here is true
don't give up and restart:
Invent a dozen acronyms HMB2, HBM2E, TC-NCF,
MR-UF, MUF, MR-MUF and try them all.
How SK hynix Won the AI Memory Race
https://www.youtube.com/watch?v=Cg5tAujp6Go
Bye
Mild Shock schrieb:
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 Günter 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.
>
Les messages affichés proviennent d'usenet.