Re:Terence Tao, "Machine Assisted Proof" [video]
by pfdietz on Wednesday February 14, 2024 @11:23PM
(#39379083)
Ah, but the nice thing about constructing formal proofs is you can immediately tell if the output is correct.
[ Parent
| on HN ]
Re:Terence Tao, "Machine Assisted Proof" [video]
by practal on Thursday February 15, 2024 @10:59AM
(#39384288)
Yes, but you also need to make sure the input is correct! For example, your idea of automatically formalising a paper needs to somehow make sure that the result means the same as the paper.