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.
There is no evidence to substantiate what you are saying.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.
Is there a proof that every possible proof is a generation in the grammar of lean or rocq? Sounds like an unsubstantiated claim.
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 ↗