-3

But Timothy Gowers, a mathematician and Fields medalist at the University of Cambridge, wants to go even further: He envisions a future in which theorem provers replace human referees at major journals. “I can see it becoming standard practice that if you want your paper to be accepted, you have to get it past an automatic checker,” he said.

Stephen Ornes, How close are computers to automating mathematical reasoning?, Quanta Magazine, August 27, 2020.


Is anything like this being done? I'm inclined to say it is, if they already have the tools, even if they don't publicly admit it.

0

3 Answers 3

21

There's literally zero chance any journal is doing anything like this. There's been exactly one instance of serious computer verification of a substantial portion of cutting-edge research within the timeframe of the refereeing process, and it's the Liquid Tensor Experiment where a group headed by Johan Commelin verified a key portion of new results of Clausen-Scholze. It was a big surprise to a lot of people that this was possible, and it's certainly not being done routinely or secretly.

2
  • 12
    Math papers are full of sentences like "By a routine argument similar to that in the proof of [13, Theorem 2.3], it follows that..." A human who is familiar with [13, Theorem 2.3] can come up with the argument. Computers are nowhere near that skilled. You might ask why mathematicians are allowed to write these vague hints at arguments in their papers instead of actual arguments - the answer is that you really don't want to turn what are now 30 page papers into 300 page papers, and it's actually easier for an expert to reconstruct the argument from the hint than to read it. Jul 28, 2021 at 1:53
  • 19
    @JoeD - You're misinterpreting what happened in this case. What happened is that some mathematicians who are not the authors took the proofs from the paper, expanded them into a form that could be understood by the computer, and then had the computer check them. This is far from an automated process. Jul 28, 2021 at 1:59
8

What Timothy Gowers suggests can't be done in secret or as a simple add-on to an otherwise unchanged review process at the current stage of technology.

The suggestion, as I understand it, is that at some point in time, journals may require authors to submit along with a traditional article a machine-checkable proof of the correctness of the claimed results. The author would, hence, work with a proof assistant to produce a formal proof of a formalized version of their main results. Successful verification of the formal proof would then allow reviewers to focus on assessing the novelty and importance of the results, without having to worry about correctness too much. They would still have to be convinced, though, that the formalizations of any results given are really formalizations of the theorems shown in the paper under review.

I think for this to happen the work factor of formalizing a typical mathematical proof would either have to fall to a level not much larger than writing up the paper (assuming that at least one of the authors is skilled in working with a proof assistant), or the production of a formalized proof would have to become a routine part of doing research. In the latter case, submitting a formal proof of one's results would be similar to submitting source code as supplementary material to a computer science paper.

For either of these to happen, proof assistants would have to become much more powerful and intuitive to use than they are today. That does not necessarily imply, though, that sufficiently useful proof assistants will only be available in the far future. Fully automated machine translation, for instance, has gone from being regarded a fairly intractable problem to being a problem with good, widely available solutions in just a few years.

The problem of automatically verifying claims in a paper written in natural mathematical language is substantially harder still. I would be tempted to say that achieving this probably requires human-level AI, but on the other hand one has to admit that previous claims of AI-completeness have failed in various domains.

The romantic notion that mathematical reasoning is based on some miracle that can only happen in human brains is, however, nonsense of course.

1
  • That verifying math requires human-level AI is perhaps incorrect; the vast majority of humans cannot verify say, a proof of the fundamental theorem of calculus. Aug 1, 2021 at 10:43
7

Probably not.

Scientific papers, even papers in mathematics, are written in natural language - sometimes fairly idiosyncratic natural language, at that. In order for an automated theorem solver to solve a theorem, the theorem will need to be rendered into a form of structured data that the computer is able to understand. While I'm not too familiar with them, I imagine that it probably involves the mathematician manually entering all the different variables and parameters into the solver, right?

Natural language comprehension by computers is currently fairly primitive, and is largely limited to the computer determining things like that certain words are more likely to occur in combination with other words, rather than demonstrating any true understanding of their meanings. As a result, getting a computer to parse a scientific paper written in natural language would be a very difficult task!

2
  • But aren't there some parts of it that would work? Not the entire paper obviously.
    – user143247
    Jul 28, 2021 at 0:56
  • 4
    @JoeD Even the parts of the paper involved in describing mathematical claims would still likely involve a lot of natural language; even if LaTeX might be more structured that plain text, how is your automated proof checker supposed to know what sort of meaning you've given to your various mathematical symbols? Maybe "delta" means a derivative, maybe it means the difference in values between subsequent values in a series, maybe it means something else altogether. That's where context comes into play, and computers are really bad at reasoning about context.
    – nick012000
    Jul 28, 2021 at 1:08

You must log in to answer this question.