Hacker News Reader

Comment by benrbray | Hacker News Reader

This is quite interesting, especially since one of the major objections to computer-aided proofs has that they are more difficult for humans to understand.

Common wisdom has been that proof techniques matter more than the results, but if human-authored proofs are no longer being inspected, it seems like it's just a matter of time before computer-aided proofs take over. I wonder how long it will be before proof assistants (like Lean, Coq, etc.) become ergonomic enough that the average non-technical math researcher will feel social pressure to publish a computer-aided proof along with their result.

View on HN

I think it will be quite some time yet. As a researcher, my objection to computer-aided proofs is not that they're hard to read -- you would of course write a human readable version to go with it -- but rather that they're extremely time-consuming to write. (And writing papers is hard enough already.)

A typical research paper is written at a very high level; often steps in the argument will assume the reader is also a skilled mathematician, and invite them to fill in the lower-level details themselves. This reasoning is as much intuitive as it is formal; I suspect it will be a while before proof assistants are as intelligent as the typical reader of a mathematics paper.

I think there's an outside perspective that if math isn't 100% logically verified, it's worthless, which doesn't really match up with my own experience. Most results rely more on the intuition of the authors than on the precise logic they write down; thus the surprising result that papers with logical gaps are, very often, still correct.

That's basically what I meant by "ergonomics" -- do you think we're still quite far from researchers being able to develop their own "tactics" to automate the sort of reasoning that would normally be "left as an exercise" to the reader of a research publication?

Yeah, "left as an exercise" can mean anything from "this is an undergraduate exercise" to "if you understand both the field and this paper, you could write a different, much longer paper, and we both know this, so let's assume I wrote that one."

It's probably not impossible to build a proof language that makes that kind of thing doable, but I suspect that (a) it would be genuinely difficult to operate it skilfully, much as being a really good developer is difficult, and (b) it would take a huge collective effort on behalf of each research community to prove the foundational results everyone relies on.

Whereas the system we have right now, despite sounding kind of weird to outsiders, mostly works okay? I'm just not sure a switch to formal proofs would be worth the time investment -- or that you could convince the many researchers less interested in tech than myself.

I came here to say that maybe it makes things simpler though when everyone speaks the same language, and all proofs are written in the same format.

However then I remembered the new codebase I inherited and OMG it's such a mess because somehow just converting a UI enum to a DB enum is a 25-line function that's repeated over and over everywhere. (Needs to be version-safe for different clients that may have old enum values, needs to create error message in appropriate language, etc, and the callers are in different layers and all have different ways of getting the corresponding info).

So yeah maybe the high-level "I get it, you get it, we all get it, let's just state this an move on" is better.

The main objection to computer-aided proofs is not that they are more difficult for humans to understand.

The main objection is that most proof-assistants use a different logical foundation than modern mathematics. Modern mathematics is built on ZFC[0] whereas most proof assistants, such as Coq, Isabelle, Agda, etc use different logical foundations, such as the Calculus of Constructions[1].

Many important results in modern mathematics are not easily stated or proven in systems such as CoC[1]. For example, Brouwer's _Fixed Point Theorem_[2], a pretty bog standard result in Topology that is useful to proof many things in Functional Analysis, has a clear statement in ZFC, but does not, to my knowledge, have an equivalent in CoC (and if it does it will be stated radically different).

[0]: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... [1]: https://en.wikipedia.org/wiki/Calculus_of_constructions [2]: https://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem

This is an explicit goal of one of of the creators of homotopy type theory, Fields medalist Vladimir Voevodksy: https://www.ias.edu/ideas/2014/voevodsky-origins

Apparently he now uses Coq in his everyday work.

He's been dead for four years?

Apparently he didn’t shut down his computer before he died.

Dat uptime tho

Oh snap, I had no idea that he died! Wow... that's a profound loss for the field of mathematics.

Reply on news.ycombinator.com