AI is not AGI right now, it can't think or come up with something new like a human brain. It still uses knowledge that was made by a human and was published on the Internet.
You're confusing the mechanical language of math with math itself.
The map is not the territory, etc.
If math was just an elaborate linguistic Glass Bead Game then we wouldn't be funding it. The intuition is that the surface rules of math help uncover the underlying structure of reality.
While every formal proof can be encoded mathematically that doesn't imply that the grammar of lean or rocq is sufficient to encode every potential proof.
However the core of what you are saying: that every possible proof exists in the space of all mathematical statements is correct.
You are correct, but in trying to get the point across I attempted (perhaps fruitlessly) to use concrete concepts today of a system where the search space is calculable yet whose span does not imply the 'knowing' of all calculable things.
0xEnsp1re · · focus · HN ↗
anon291 · · focus · HN ↗
Every possible proof exists already as a possible generation in the grammar of lean or rocq. In no way does that mean we have discovered everything.
goatlover · · focus · HN ↗
otabdeveloper4 · · focus · HN ↗
The map is not the territory, etc. If math was just an elaborate linguistic Glass Bead Game then we wouldn't be funding it. The intuition is that the surface rules of math help uncover the underlying structure of reality.
nl · · focus · HN ↗
While every formal proof can be encoded mathematically that doesn't imply that the grammar of lean or rocq is sufficient to encode every potential proof.
However the core of what you are saying: that every possible proof exists in the space of all mathematical statements is correct.
anon291 · · focus · HN ↗