logoalt Hacker News

refulgentistoday at 3:28 AM1 replyview on HN

But isn't that tantamount with "his comment is a complete non-sequitor"?


Replies

Paracompacttoday at 4:57 AM

I don't think so? Lean is formal methods, so it makes sense to discuss the boons of formal and semiformal methods more generally.

I used to think that the only way we would be able to trust AI output would be by leaning heavily into proof-carrying code, but I've come to appreciate the other approaches as well.

show 1 reply