On: Can the language of proof assistants be used for g...

[schoen]

Adding a large language model is going to move you in the exact opposite direction from ease of formal verification.

[epgui → schoen]

I mean... Not necessarily? It depends how you use it or what part of the process you delegate to it, no?

Whether AI produces Lean code or a human produces Lean code... The Lean code should speak for itself. Both humans and AI are the weak link in either case, and it's unclear to me which of the two is the weaker.

[schoen → epgui]

Oh, I think I misunderstood the proposal there. I thought the language model was meant to be producing (only) code, not proofs.

If it manages to produce successful proofs of pre-existing property specifications, then that's great!

[ratmice → schoen]

Yeah, I think the catch is the "pre-existing property specifications" part. I think you need to carefully understand both AI & Human generated propositions. While proofs once checked are just gravy.