Hi,
Accelerate Lean! And get from Theorem 3.11
to Corollary 3.12 done.
PROJECT LANA INTERIM REPORT ON IUT THEORY
ZEN Mathematics Center - 2026/07/17
https://zen.ac.jp/en/zmc
ZMC?ZEN Mathematics Center) is an international
research institute established with the aim
of promoting and developing modern mathematics
with a focus on arithmetic geometry and the
formalization of modern mathematics using
computer languages
LoL
Bye
Mild Shock schrieb:
Hi,
Maybe I should write a blog post, titled
Introduction to AI Accelerator Prolog:
- specialized jobs ã-WAM (currently integerish stuff)
- ã-WAM uses no atomics, only comms
- ã-WAM uses warp, 30-40% more speed
- ã-WAM runs on GPU and CPU
- ã-WAM runs from within JavaScript, Python and Java
Feels like reinventing FGCS concurrent
logic programming.
LoL
Bye
Mild Shock schrieb:
Hi,
So the idea is to cover backtracking without
stack and choice points, only with registers.
So at the compute goto will use an instruction
that stores the PC target into a register,
a new instruction for Hack:
REG = PC + REL
And then the jump will be, again a new
instruction for Hack:
PC = REG
If we squeeze the lemon and compile as much
with that, we will only find that it breaks for
calling recursive predicates that can use
arbitary registers and choice points. But we
could maybe add stack and choice point as an
after match, instead of the classical WAM design
that starts with stack and choice points!
Bye
Mild Shock schrieb:
Hi,
pi-WAM is a nice challenge, since its aim is to go
even blow the instruction set of SWI-Prolog,
while only using a Hack variant as instruction
stream. But what is Hack? Well Hack seems to be
the missing legacy of Niclaus Wirths PL0. The
Hack (machine .asm) and Jack (highlevel compiler
generating .vm which can be converted to .asm)
combo makes even the famous Crafting Interpreters
/Lox by Bob Nystrom redundant:
Nand to Tetris courses are taught at 400+
universities, high schools, and bootcamps. The
students who take them range from high
schoolers to Ph.D. students to
https://www.nand2tetris.org/
But digging deaper in Hack, it has no functions
pointers so objects don't use virtual tables.
But what will pi-WAM need and that is not yet
in Hack? Given that my pi-WAM doesn't want a stack
nor a choice point lists? Currently there is the
idea to add a computed goto and that it can
cover a more lightweight C_OR as known from
SWI-Prolog, that would have the C_OR branches
maybe restricted to have no outside
clause calls? Lets see. Not yet sure.
Bye
Hi,
Disclaimer: I don't know what I am talking
about. But I like the vibe behind connecting
topics. So here we go:
How it started:
Gabriels Horn
Gabriel's horn, also called Torricelli's trumpet,
is the surface of revolution of the function y=1/x
about the x-axis for x>=1. It has infinite
surface area but finite volume. https://mathworld.wolfram.com/GabrielsHorn.html
How its going:
FINITE TIME BLOWUP FOR NAVIER?STOKES
or every positive viscosity, we construct a solution
of the three-dimensional incompressible Navier?Stokes
equations that starts from rest and develops unbounded
velocity in finite time while maintaining uniformly
bounded kinetic energy
Hava Fun everbody!
Bye
Hi,
Ever noticed that remaining unsolved conjectures,
are difficult to decipher:
https://en.wikipedia.org/wiki/Hodge_conjecture
Although Grothendiek claimes it is part of
his yoga on motivic rationality.
The dilemma is Humans cannot do math anymore
on that level. And AI math on the level tends
to be not understandable by humans anymore. So
its as if math has found a new muse.
The new Muse is AI. I think proving math conjectures
is the more low hanging fruit than colonizing
Mars. But the result of this endeavours is a
shocked public, now in total freeze.
Bye
Mild Shock schrieb:
Hi,
Disclaimer: I don't know what I am talking
about. But I like the vibe behind connecting
topics. So here we go:
How it started:
Gabriels Horn
Gabriel's horn, also called Torricelli's trumpet,
is the surface of revolution of the function y=1/x
about the x-axis for x>=1. It has infinite
surface area but finite volume. https://mathworld.wolfram.com/GabrielsHorn.html
How its going:
FINITE TIME BLOWUP FOR NAVIER?STOKES
or every positive viscosity, we construct a solution
of the three-dimensional incompressible Navier?Stokes
equations that starts from rest and develops unbounded
velocity in finite time while maintaining uniformly
bounded kinetic energy
https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf
are you alive or only youre spam bot here?Hava Fun everbody!
Bye
Hi,
Ever noticed that remaining unsolved conjectures,
are difficult to decipher:
https://en.wikipedia.org/wiki/Hodge_conjecture
Although Grothendiek claimes it is part of
his yoga on motivic rationality.
The dilemma is Humans cannot do math anymore
on that level. And AI math on the level tends
to be not understandable by humans anymore. So
its as if math has found a new muse.
The new Muse is AI. I think proving math conjectures
is the more low hanging fruit than colonizing
Mars. But the result of this endeavours is a
shocked public, now in total freeze.
Bye
Mild Shock schrieb:
Hi,
Disclaimer: I don't know what I am talking
about. But I like the vibe behind connecting
topics. So here we go:
How it started:
Gabriels Horn
Gabriel's horn, also called Torricelli's trumpet,
is the surface of revolution of the function y=1/x
about the x-axis for x>=1. It has infinite
surface area but finite volume. https://mathworld.wolfram.com/GabrielsHorn.html
How its going:
FINITE TIME BLOWUP FOR NAVIER?STOKES
or every positive viscosity, we construct a solution
of the three-dimensional incompressible Navier?Stokes
equations that starts from rest and develops unbounded
velocity in finite time while maintaining uniformly
bounded kinetic energy
https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf
Hava Fun everbody!
Bye
The new Muse is AI. I think proving math conjectures
is the more low hanging fruit than colonizing
Mars. But the result of this endeavours is a
shocked public, now in total freeze.
Hi,
I guess Kurzweils transhumanism is also not
on the list of the low hanging fruits of AI.
Moreover this turns out to be a fallacy:
| Sysop: | Tetrazocine |
|---|---|
| Location: | Melbourne, VIC, Australia |
| Users: | 8 |
| Nodes: | 8 (0 / 8) |
| Uptime: | 14:42:35 |
| Calls: | 220 |
| Files: | 21,513 |
| Messages: | 83,058 |