|
At one point during my PhD, I proved a fairly technical theorem, which generalized a result from 1996. Both my result and the 1996 result used techniques from nonstandard analysis. About 6 months later, an article appeared on arXiv, and pointed out that the 1996 proof had a flaw in it (fortunately, the result did hold, but the proof required some modification). I felt terrified: I was using very similar techniques, but as part of a more complicated proof. I couldn't guarantee that I didn't make a similar (or worse) mistake. So I sat down with the Agda proof assistant, and wrote about 4000 lines of code to verify the theorem I proved (Agda differs from ACL2 quite a bit, and I ended up developing an extension to Martin-Löf type theory so that I could formalize this style of reasoning effectively). This reassured me that my result was correct, and it made for a nice chapter in my thesis. And it convinced me that nonstandard analysis synergizes very effectively with both automated and interactive theorem proving. Nonstandard analysis helps automated theorem proving by keeping quantifier complexity [1] low. Statements that have many quantifier alterations. Statements that have many alterations of quantifiers are more difficult to handle than ones with fewer quantifier alterations: young children can frequently grasp the definition of monotonicity (no quantifier alterations, "for all x and y, ..."), but they have a much harder time with continuity (2 quantifier alterations, "for all x and for all ε, there is some δ such that for all y"). The same holds for machines: they have a much easier time if quantifier complexity is kept low. Nonstandard analysis accomplishes that in many settings: for example, you can use it to express continuity without quantifier alterations. Nonstandard analysis helps interactive theorem proving in multiple ways. Just like in automated theorem proving, it lowers quantifier complexity, and it makes it easier to express certain definitions. But nonstandard analysis also improves "code reuse": certain combinatorial theorems imply their "infinite counterparts" via a few lines of nonstandard analysis. This is not that important or useful in informal, pen-and-paper mathematics, since the finite and the infinite theories developed in parallel, and tend to be equally developed as a result. But it comes in handy when we do interactive theorem proving: some areas of mathematics have not been formalized yet, and formalizing all the bits of "infinite" theory that you need for your result may take a long time. In many cases, a tiny bit of nonstandard analysis can help us sidestep such issues. Synergy goes both ways, in that interactive theorem proving helps nonstandard analysis too. There are very few people who are familiar with the techniques of nonstandard analysis, so it can be hard to find people who can proof-read or referee new works. And since nonstandard analysis (both the IST formalism used in the linked article and the model-theoretic approach) relies on syntactic restrictions, accidental mistakes in nonstandard analysis proofs have a distinct "flavor", different from most other areas of mathematics. This means that reviewing requires a bit more care than usual. Proof assistants and proof checkers are incredibly useful here. [1] https://mathoverflow.net/questions/281894/examples-of-statem... |