4 ms·
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
by epgui 3y ago
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 3y agoOh, 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 3y agoYeah, 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.