2 ms·
In the same spirit of this talk, good HN post https://news.ycombinator.com/item?id=38035672 https://news.ycombinator.com/item?id=38035672 on Terry Tao's use of
by the_panopticon 3y ago
In the same spirit of this talk, good HN post https://news.ycombinator.com/item?id=38035672 https://news.ycombinator.com/item?id=38035672 on Terry Tao's use of proof assistants and LLMs to find a paper bug https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...