Hacker News Reader

Comment by bmitc | Hacker News Reader

I am of the opinion that mathematics is very much a human endeavor. Writing a proof is to convince other mathematicians that it’s true. While formalized mathematics is one such technique, I don’t believe it will replace how mathematics is generally done. Writing a program is something different entirely.

One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.

View on HN

A verified proof is a very convincing argument.

I am not against including a human focused discussion of a proof, stepping through it in human terms. A verified proof is more like the final step or output.

I agree this is not how maths is done, there is a huge exploration stage. People do not just crank out a proof even though sometimes it is written in a way to make you believe that. You can spend days, weeks, months exploring. But at some point you should try to formalise that into something coherent.

Amendment: this seems to be a very controversial discussion with wildly swinging upvotes/downvotes. I hope people would elaborate on their viewpoints.

Proofs are more about understanding why something is true, than verification per se. See this well known article by the illustrious Bill Thurston (RIP):

https://arxiv.org/abs/math/9404236

The free refactorability of a fully formalized proof can provide a lot of additional understanding, compared to an informal sketch.

I think it’s all great. I have been interested in picking up something like Coq before. I only made my comment to reflect my personal tempered expectations. Maybe I am completely wrong, but just don’t see how it could wholly replace how mathematics is done and generated, but I do see how it could helpfully augment. I think the analogy is in the fancy type system programming languages like Haskell and Idris and the like, which are not practically affecting how people generally write programs and build systems.

In both mathematics and writing programs, one must come up with something that models the solution needed for a given problem or system even if one can formally verify it afterwards, but that first part is the hard part (especially in programming since the assumptions in mathematics are quite explicit and known). I suppose there could be or are systems that generate techniques and proofs rather than merely verify, but I can only imagine that being an intractable problem and one not likely to be practically solved soon.

Yes, the stack of papers at my desk with random scribbles are a far cry from a verified proof written in lean. There is lots behind a proof that you don't necessarily see reflected in a piece of code/proof. So I agree, something formal is like a final step.

Mathematics is not Computation. Mathematics is about stating definitions and prove theorems about those definitions. A mathematician doesn’t care whether those definitions are computable. Take a look at the leading edge (the mathlib community using the Lean prover). A lot of their definitions are non-computable and it works fine.

I am of the opinion that software development is very much a human endeavour as well ;-)

I rather read some thing that's formal and readable, than just merely readable.

> One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.

~Goëdel~ Gödel's theorems are not relevant. Consider even if the halting problem had the other answer, it still could be impractical to do the brute force search. Same thing here.

And frankly, the formal methods community is sick of people spreading FUD from that stuff. Mixing romantic humanism with technical misunderstandings is no good.

It is spelled Gödel or (in case you cannot put the 2 dots over the "o") Goedel.

Yes thank you. I guess I mixed up US keyboard vs phone typing rather hilariously.

I didn’t mention Goedel’s theorems, so I don’t know what they’re relevant or irrelevant to, and I am not spreading anything.

Maybe I didn’t make that part clear, but it’s more of a question of mine than a statement. It seems to me there would be problems and limits but I haven’t seen them addressed in a way I understand, so the questions and misunderstandings remain.

If you have any references, then by all means share them.

> Mixing romantic humanism with technical misunderstandings is no good.

I think this miscategorizes what I wrote. One could easily do the same.

Mathematics is indeed a human endeavor, as are its goals. If machines are to help, then that’s absolutely great (I’m actually a big fan of computers being used to augment human endeavors), but making grand sweeping claims like I’ve seen in discussion of proof assistants is as romantic as anything.

I think the proof assistants are getting very powerful, eg:

https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...

State of the art research explored with lean. I think a certain level of hand wavy romanticism is fine for a HN comment if it can inspire people to be interested in the field. I also would prefer to be corrected in a reasonable discussion than a silent chilling downvote.

Thanks for the article/interview. I am intrigued to find Peter Scholze’s own words calling this a “human experience”.

https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...

This is actually a great article that helps to show that humans are still very much involved in convincing each other, using machines to aid to that effect.

Regarding downvotes, you can’t even downvote someone you’ve replied to or they’ve replied to you on Hacker News.

Foundations of mathematics are inferentially incomplete, that, is,

there are true but unprovable propositions (although [Gödel 1934] results do not hold for foundations).

See following for a proof:

https://papers.ssrn.com/abstract=3603021

However, inferential incompleteness does not cause practical

difficulties for proof checking assistants :-)

> Mixing romantic humanism with technical misunderstandings is no good.

What are you referring to with this comment?

Reply on news.ycombinator.com