1 comment

[ 2.7 ms ] story [ 12.4 ms ] thread
How long until an AI can do the formalization for a proof like this one fully automatically?

For example, the "direct proof" in this paper is six paragraphs long.