kdavis
Joined 14 years ago
Joined 14 years ago
But then again, he was John von Neumann.
Harsh words for someone you've had no social interactions with. To me this statement says more about you than Jack Weis.
Physicists knew Navier-Stokes was an approximation that breaks down at some scale, e.g. the molecular scale. This AI solution just exhibits such a breakdown.
That said there are some efforts in the direction you're suggesting. For example
- [Prove2Me](https://beta.prove2.me) - Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. One creates open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.
- [Tau Ceti](https://github.com/TauCetiProject/TauCeti) - An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
Early 80's I learned Logo and Basic at a local store that sold Apple computers. It was called "The Logical Choice" and had a classroom tucked away behind a false wall and an English Sheep dog "Sir Isaac Newton" that would hang around the store!
Nice, I just found a story on the store, page 5 of [1].
[1] https://mirrors.apple2.org.za/ftp.apple.asimov.net/documenta...
For example, in the Unruh effect an inertial observer sees the vacuum in their Hilbert space as having no particles. However, a uniformly accelerating observer sees that same vacuum as containing particles.
This state of affairs is addressed via algebraic quantum field theory (AQFT), which doesn't take a Hilbert space as the primary thing one starts with, but views Hilbert spaces as derived concepts.