Re:Mathematicians welcome computer-assisted proof in ‘grand ...
by foooobar on Saturday June 19, 2021 @03:42PM
(#27563749)
As far as I can tell, this is not quite true. Tactic proofs aside, you can also write functional term mode proofs and declarative "structured" proofs in the sense of Isar. Theorem Proving in Lean introduces that style, so most people who use Lean are familiar with it: E.g. https://leanprover.github.io/theorem_proving_in_lean/proposi...
Additionally, even in tactic proofs you can use tactics like `have`, `suffices`, etc. to manipulate the structure of the proof and make subgoals explicit like you would usually do in the structured style. In practice, people in Lean still prefer imperative tactic proofs with the option to write in a structured/declarative style where reasonable. The full "structured" mode does not see much use, since it is quite verbose. As a result, Lean 4 will not support this style out of the box anymore, but you could still add it yourself using the macro system.
This is an issue, but there's an established practice of writing formal sketches where the gaps in the proof are explicitly marked, and future tooling might bring ways to address these gaps once a full formal context is provided.
One issue is that Lean has little or no support for declarative proof, which is by far the most natural setting for these "proof sketches", and also brings other advantages wrt. complex proofs. (Coq has the same issue; some code was written to support declarative proofs, but it was too buggy and bitrotted, so it got removed.)