4 ms·
The checking has nothing to do with AI, despite the (massively funded) marketing done to make you think so. It is based on formal methods/theorem provers.
by InkCanon 4mo ago
The checking has nothing to do with AI, despite the (massively funded) marketing done to make you think so. It is based on formal methods/theorem provers.
- dellamonica 4mo agoThe point of the AI with respect to checking is to translate a natural language theorem and its proof into the formal system. Most of known math is not formalized because it is very hard to do so.
- world2vec 4mo agoFrom what I've seen on Tao's YouTube channel, he does use GitHub Copilot via VSCode to write Lean4 code.