But they do plan to release the Astra model to the public "after it's finished" I assume?
And yeah this Lean software sounds amazing, didn't know this was possible.
I misread your last sentence in a way that create a different problem: Imagine AI starts producing more and more proofs at a pace that humans can't keep up with. So science advances, and humans can even make use of it, but can't verify or really understand the theory any more. Like we get better working machines, materials and processes, but do not understand why because we can't keep up. If that happened then that I guess would a significant stage in the singularity.
It's a "category error" like saying hydrodynamics are just quantum mechanics. It does not describe the complex emergent behavior and doesn't really tell you anything. Or it's like saying psychology is how the neurons and synapses connect with each and exchange signals and that is all - this would not explain the mental processes between a marmot and a human. So it's not an accurate simplified description, just a description of the basic building blocks.
Afaik nobody knows how LLMs actually think, we only know sort of how to train them. They are researching how LLMs think with an equivalent to MRI brain scanning: Vista do LLM-MRI Python module: a brain scanner for LLMs