Hacker News Reader

Comment by lordnacho | Hacker News Reader

Noob question here.

Say I'm wanting to formalize a proof. How do I know that what I'm writing is actually a correct formulation?

If it gets more complicated, this problem gets worse. How do I know the thing it is checking is actually what I thought it was supposed to check?

I guess this is a bit like when you write a program and you want to know if it's correct, so you write some tests. But often you realize your tests don't check what you thought.

View on HN

You don't know. Even with the best theorem provers, your definitions are still trusted. The best way I've found to help with this is to keep your definitions simple, and try to use them to do things (e.g. can you use your definition to solve other problems, does it work on some concrete examples, etc).

A point that is maybe not obvious to people who have not done mathematics at a high level or done “new” mathematics, is that often you end of changing your theorem or at least lemmas and definitions while figuring out the proof. That is, you have something you want to prove, but maybe it is easier to proving something more general or maybe your definitions need to change slightly. Anecdotally, during a project I spend perhaps a year figuring out exactly the right definition for a problem to be able to prove it. Of course, this was a very new thing. For well-know areas it is often straight forward, but at the frontier, both definitions and theorems often change as your proceed and understand the problem better.

Being sure that you are proving the right thing is something that can never be formally guaranteed.

In a lot of cases you can get far by locally proofreading the definitions.

Trying to formally prove something and then failing is a common way people find out they forgot to add an hypothesis.

Another pitfall is defining some object, but messing up the definitions, such that there's actually no object of that kind. This is addressed by using test objects. So suppose you define what a ring is, then you also prove that real numbers and polynomials are examples of the thing you defined.

Reply on news.ycombinator.com