101–110 of 140 posts
But as things look now, I will be willing to bet that the next major breakthrough in maths will be touted as being AI/LLMs and coming out of one of the big US tech companies rather than some German university.
Why? Simply, the money is much bigger. Such an event would pop the market value of the company involved by a hundred billion - plenty of incentive right there to paint whatever as AI and hire whoever.
I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
So, you looking for Cyc [1], practically. [1] https://en.wikipedia.org/wiki/Cyc
Earlier quoted context omitted.
Does Cyc have proofs?
In a sense, yes, since it has a foundation in Prolog style facts and rules, and supposedly can output its reasoning.
Are there any checks for the consistency of all facts?
Earlier quoted context omitted.
In a sense, yes, since it has a foundation in Prolog style facts and rules, and supposedly can output its reasoning.
Ok, sounds like in principle you could have proofs, but in practice, you don't? Are there any checks for the consistency of all facts?
Is it currently possible to reliably limit the cut-off knowledge of an LLM (either during training or inference)? An interesting experiment would be to feed an LLM mathematical knowledge only up to the year of proving a theorem, and then see if it can actually come up with the novel techniques used in the proof. For example, having only access to papers prior to 1993, can an LLM come up with Wiles' proof of FLT?
Is it currently possible to reliably limit the cut-off knowledge of an LLM (either during training or inference)? An interesting experiment would be to feed an LLM mathematical knowledge only up to the year of proving a theorem, and then see if it can actually come up with the novel techniques used in the proof. For example, having only access to papers prior to 1993, can an LLM come up with Wiles' proof of FLT?
Mathematicians have been using computers, programming languages, and proof engines for over half a century; however breakthroughs in mathematics are still made by humans in any meaningful sense, even though the tools they use and make are increasingly complex. But as things look now, I will be willing to bet that the next major breakthrough in maths will be touted as being AI/LLMs and coming out of one of the big US…
Earlier quoted context omitted.
Ok, sounds like in principle you could have proofs, but in practice, you don't? Are there any checks for the consistency of all facts?
How could there be? Gödel gets in the way.
If Cyc has 100000 axioms/facts, then that's a problem.
Earlier quoted context omitted.
Probably a bad example, P vs NP is the most likely of the millennium problems to be unsolvable, so the answer may be "never". I'll bet the most technical open problems will be the ones to fall first. What AIs lack in creativity they make up for in ability to absorb a large quantity of technical concepts.
Ok, then the AI should formally prove that it's "unsolvable" (however you meant it).
Then again, it's fairly likely that P=?NP is decidable but we just don't have any idea how to prove it. In that case the question is more or less "what's the time horizon until AI is vastly better than humans at formal math?", to which the answer is certainly "we don't know, there may be obstacles, just wait and see".