<div dir="ltr"><div>Mathematics has used informal proofs for thousands of years, and this is why we made progress because the cost of a formal proof is enormous.</div><div>Why then use agda? Because types can guide the implementation of parts that are important or are part of the computational path.</div><div><br></div><div>The question then is to find the correct strategy:<br></div><div>A) Informally prove a proposition and put explicitly the postulate assumptions in the type. Have a secondary proposition without those assumptions. This is the one to be used by the other proofs.<br></div><div>B) One could use type variables to imitate the traditional informal way of proving. ("Because of theorem1.1 , lemma2.4 etc.")</div><div>C) Avoid proofs inside the types as much as possible, use abstraction if the proof is used in the arguments and existential quantification if it is used in the type of the result.</div><div><br></div><div>The question then becomes how to limit the effects of a failure of a proof of a proposition. Will the effects cascade to the all the remaining proofs? Many times ,</div><div> the failure can be local and mitigated with a fix. In others, the effect is catastrophic. </div><div><br></div><div>For example, Shinichi Mochizuki's proof of the abc conjecture could be wrong because of the incorrectness of a corollary. Given that the theory is thousands of pages and many years of work, this will certainly be a catastrophic failure if one is not able to replace that proposition with something else.</div><div><br></div><div>Is the cascading effect of a wrong agda proposition bigger than in an informal mathematical setting? What are your strategies in mitigating it assuming that you use postulates?<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jan 16, 2019 at 12:49 PM Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 16/01/2019 00.56, Apostolis Xekoukoulotakis wrote:<br>
> Do you use postulates extensively?<br>
<br>
No, but I can imagine that this depends on what you are working on. If<br>
your subject of study depends on a lot of prior, very solid work, then<br>
it might make sense to use postulates.<br>
<br>
When I prove something under an assumption that cannot be proven (say,<br>
"assuming equality of functions is extensional…") I have found it useful<br>
to state the assumption explicitly rather than using postulates. This<br>
makes it easy to track exactly what parts of the development depend on<br>
what assumptions.<br>
<br>
-- <br>
/NAD<br>
</blockquote></div>