← Back to context

Comment by refulgentis

8 hours ago

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

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.