This is analogous to "sorry" in Lean. "The sorry identifier magically produces a proof of anything, or provides an object of any data type at all. Of course, it is unsound as a proof method – for example, you can use it to prove false – and Lean produces severe warnings when files use or import theorems which depend on it. But it is very useful for building long proofs incrementally. Start writing the proof from the top down, using sorry to fill in subproofs. Make sure Lean accepts the term with all the sorry’s; if not, there are errors that you need to correct. Then go back and replace each sorry with an actual proof, until no more remain."
https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html#propositions-as-types On Thursday, August 20, 2020 at 2:00:49 PM UTC+3 Anarcocap-socdem wrote: > Let us imagine I want to solve a problem (probably the argument would be > the same to proof a theorem, but I "see" this argument better applied to > problems and exercises than to theorems). > > I know how to solve the problem: the solution depends on say three > well-known theorems, and just applying the axioms of predicate calculus in > a reasonable way. The amount of steps is reasonably low. > > So, if these three theorems were proved in metamath, everything would be > easy. > > However, it could be that these theorems are not proved in metamath (this > is another question: how reasonable it is that metamath eventually covers > an undergraduate degree material? Will the modularity, i.e. using > metamath-proven theorems, eventually explode up the amounts of content in > metamath? Or will proofs become more and more complex, even within an > undergraduate level, without the possibility to apply modularity to them?). > > One possibility is to abandon the project to provide the solution of the > problem with metamath. But another possibility would be to try and > "convert" the three theorems into some kind of definitions or axioms. Then, > these three theorems would be true by definition, and one would only need > to apply the axioms of predicate calculus to really solve the problem. > > Does this approach make any sense? For proof of theorems, probably not, > since there could eventually be a doubt whether a theorem had been really > proved, or if it had been "proved" via "defining/axiomatizing" the hard > parts of the proof. This would be unacceptable. But for problems/exercises, > this should never(?) be a problem, I think. > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a47cda16-3bf4-4e9f-86a9-a06cb9887f53n%40googlegroups.com.
