[sabujp]

    "Proof assistants can’t read a maths textbook, they need continuous input from humans, and they can’t decide whether a mathematical statement is interesting or profound — only whether it is correct, Buzzard says. Still, computers might soon be able to point out consequences of the known facts that mathematicians had failed to notice, he adds."

we're closer to this than people realize

[kevinbuzzard]

I agree, but I think my statement is accurate today in 2021. I would love to see funds directed towards this sort of question. The big problem is that at high level so so much is skipped over, and you still sometimes have to struggle to put undergraduate-level mathematics into Lean -- this is why UG maths is such a good test case.

[mherrmann]

Very nice to see you here Kevin. We never interacted but I do still remember a lecture you gave at Imperial in '06 where you filled in for Prof. Liebeck and started with Lemma 1: "I am not Professor Liebeck" ;-) Thank you for the nice memory and your important work on / with Lean.

[ninguem2]

Did he prove the lemma or did he leave it as an exercise :-) ?

[zozbot234]

> The big problem is that at high level so so much is skipped over

This is an issue, but there's an established practice of writing formal sketches where the gaps in the proof are explicitly marked, and future tooling might bring ways to address these gaps once a full formal context is provided.

One issue is that Lean has little or no support for declarative proof, which is by far the most natural setting for these "proof sketches", and also brings other advantages wrt. complex proofs. (Coq has the same issue; some code was written to support declarative proofs, but it was too buggy and bitrotted, so it got removed.)

[foooobar]

As far as I can tell, this is not quite true. Tactic proofs aside, you can also write functional term mode proofs and declarative "structured" proofs in the sense of Isar. Theorem Proving in Lean introduces that style, so most people who use Lean are familiar with it: E.g. https://leanprover.github.io/theorem_proving_in_lean/proposi...

Additionally, even in tactic proofs you can use tactics like `have`, `suffices`, etc. to manipulate the structure of the proof and make subgoals explicit like you would usually do in the structured style. In practice, people in Lean still prefer imperative tactic proofs with the option to write in a structured/declarative style where reasonable. The full "structured" mode does not see much use, since it is quite verbose. As a result, Lean 4 will not support this style out of the box anymore, but you could still add it yourself using the macro system.

[gwern]

It's worth noting that GPT-f already gets a big performance boost from pretraining on Arxiv etc (https://arxiv.org/pdf/2009.03393.pdf#page=7) despite those sources containing next to no Metamath or anything that looks like a raw Metamath proof, just regular natural language & LaTeX discussing math...

[astrange]

How well does text extraction from a PDF work? I almost never try it but thought there were random spaces in the output and such things.

[hangsi]

A fair summary would be "often very well, but not always". A good exmaple would be the S2ORC dataset [0]: a dataset of full parses of scientific PDFs. In their paper, the authors write about the difficulties of getting the parsers to work reliably, and how having multiple published versions of a PDF was helpful for when the PDF parser fails on the first one.

[0] https://allenai.org/data/s2orc

[moyix]

It's worth noting that for most papers, arXiv provides the LaTeX source for download, which is presumably what they trained on.

[amelius]

> we're closer to this than people realize

At least give a proper reference to what you're alluding to, please.

Also, closeness in AI has shown to be a misleading concept.

[gerdesj]

A reference you might like to note is in a response - that kevinblizzard bloke probably has a fair old handle on this stuff. Note how he is quoted throughout the article.

This is about some pretty creative uses of computing in maths and bugger all to do with AI (whatever that is.)

If you put enough blood, sweat and tears into codifying mathematical concepts into Lean, you can feed it a mathematical thingie and it can tell you if that thingie is correct within its domain of knowledge. If you get an "out of cheese error", you need to feed it more knowledge or give up and take up tiddlywinks.

This explains Lean in terms I can understand: https://www.quantamagazine.org/building-the-mathematical-lib...

[AtlasBarfed]

Simply having a linked graph of related concepts might show "impact diffs" in theorems.

I recall that the Fermat's proof linked several normally disparate areas to get to the meat of the issue.

Simply tagging those relations to identified sub-fields of study will probably help give guidance to impacts of theories, maybe farm them out to advanced students for quick review.

[GPerson]

Why do you say this?

[kevinbuzzard]

I'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine, and get a Lean proof of Fermat's Last Theorem.

[wolverine876]

I think the GP might have been responding to the GGP, not to your statement in the article.

[throwaway81523]

I remember asking Bob Solovay whether he thought Wiles' proof of FLT was within reach of formalization and he said something like: it is probably 20 years away. It may have been 20 years since I asked him that, and seeing this recent work with Lean makes me think FLT might also be doable, which would make Solovay's guess just about spot on.

[GPerson]

Hi Kevin,

Yes, I was responding to the person who said “we're closer to this than people realize” hoping to learn what they had in mind.

[Haga]

Can't usefulness be approximated like Google search results of old, by connectedness to other theories.