Quanta's abstract of THE PROOF IN CODE

Stream: general

[Paul Schwahn]

Hi everyone. There's an upcoming book promoted by Quanta Books (subsidiary of the Simons Foundation) which is introduced as follows:

THE PROOF IN THE CODE is the definitive account of the birth and rise of Lean, a proof assistant developed by Microsoft that is transforming the enterprise of mathematics and ushering in a new era of human-computer collaboration. Although Lean was originally conceived of as a code-checking program, a small group of mathematicians recognized its potential to become something far more powerful: the “truth oracle” that thinkers have sought for centuries, a tool to definitively verify or refute any mathematical or logical assertion, no matter how complex. This is the story of the grassroots effort to make that dream a reality. Filled with insights about the future of math, computers, and AI, THE PROOF IN THE CODE is a brilliant work of journalism by Kevin Hartnett, a leading math writer whose research and reporting offer a profound answer to a longstanding mystery: Can computers reveal universal truths? (https://www.quantabooks.org/)

I've seen people expressing their dissatisfaction with it. To quote Josselin Poiret:

This promotional introduction is probably one of the most upsetting I've ever read. Sensationalist to the point of rewriting history and erasing decades of proof assistant research, implementations and formalization projects. Maybe the book isn't as insulting to the community at large as this small blurb, but I would doubt it given Quanta's track record.

This constant aggrandizing of a few projects's achievements with no acknowledgments of what's come before and all the people contributing to the field needs to stop. It fuels that false idea that there's a definitive hierarchy in research, an idea that bureaucrats at the head of research institutions use as an excuse to silo funding into a small number of research units.

It's also just factually wrong.

We stand on the shoulder of fellow researchers, not just a couple giants.

In response to this, Jon Sterling writes

this abstract is so absurd. Fuck quanta... I think the Lean team needs to comment publicly to clarify whether they agree with this crap.

Opinions on this? Should the Lean team feel compelled to comment? I don't want to stir up any drama, but I simply couldn't help but bring it up, because I too care about the quality of journalism.

[Jon Eugster]

even "developed by Microsoft" is already wrong, isn't it? but anyways "quality of journalism" and that introduction seem to have not much in-common:wink:

[Shreyas Srinivas]

This is a sensational abstract for a book, which takes some liberties with facts (see Jon’s message above). But I think it is pretty clear that the word “truth oracle” with all its exaggeration is referring to the small kernel checking proofs, which is again not new in lean. A lot is owed to those who worked for decades on logic, type theories, math foundations, ITP development, automation etc. Even mathlib borrows several ideas from formalisations in other ITPs.

However these replies pretending that the author is talking about the entscheidungs problem are not exactly being unsensational. It is reading too much into a bit of pop science. Further it is clear that lean did have a revolutionary effect on the math community. It brought in as users, a non-trivial number of research mathematicians who weren’t primarily working on theorem prover development. This is a substantial achievement that none of the big theorem provers can claim. In my area of work, the set of ITP users was almost entirely disjoint from the researchers in this area until lean arrived, and there are very clear cultural reasons for this. There is nothing wrong in writing a book that highlights these issues even if it is disliked by the users of other ITPs. There is a nice story to be told here. I hope the authors do justice to it without belittling the efforts of everybody else.

[Shreyas Srinivas]

If anything we in computer science tend to silo ourselves into our niches. We claim that our work helps address grand challenge X(in this case theorem provers for math), and then we measure our research impact not on the application area or end users of X (math/mathematicians), but amongst our fellow researchers (other ITP folks, logicians etc). The former is deemed too practical to be considered worthy of research interest. Lean broke this mould. That is something worth talking about, and as CS researchers, it is something worth learning lessons from.

[Jason Rute]

@Kevin Hartnett

[Bolton Bailey]

Jon Eugster said:

even "developed by Microsoft" is already wrong, isn't it? but anyways "quality of journalism" and that introduction seem to have not much in-common:wink:

I am not entirely sure what the issue is with this clause, is it that it should be "developed at Microsoft"?

[Niels Voss]

I don't actually understand the situation, but I think Microsoft is definitely involved in the project but doesn't own it in a strict sense. Probably "Developed by the Lean FRO" would be more accurate. Maybe Lean 3 and the initial versions of Lean 4 were developed primarily by Microsoft Research though. Someone please correct me if I'm wrong.

[Paul Schwahn]

Thanks for your input! Personally I think it's not fair to judge a book by just a promotional abstract, but I reckon that wasn't the point of the responses to begin with - the anger was more directed at Quanta itself. The abstract does make it sound like though that Lean is "the only game in town" - not only from the perspective of a working mathematician who heavily profits from its unique community as well as Mathlib (here I would see no big issue), but also in the general context of theorem provers overall. I think the latter is the "rewriting history" part that people take issue with.
On the other hand - it's just an abstract. You can obviously not expect it to summarize a whole book. So I suppose a lot comes down to charity of interpretation, as long as the book isn't released. Still, there is room for improvement with the sensationalism...

[Bolton Bailey]

IMO I wouldn't begrudge a 6-sentence blurb from not mentioning proof assistants that the book isn't focused on. This isn't an SoK paper it's a popular science book.

[Bolton Bailey]

@Anatole Dedecker Perhaps you can explain the Microsoft point, you said in the mastodon thread "Lean was never really "developed by Microsoft" as the abstract says, rather than the main developers were affiliated to Microsoft Research". What's the difference?

[Andrés Goens]

Perhaps one very notable point here is that the primary author is not at Microsoft Research anymore, thath does say a lot... Then again, "developed by Amazon" would probably not be better (neither would "developed at the KIT or CMU" or similar).

My take is that it's a recognizable name of a big company so it goes well in a sensationalist abstract, and of all the half-truths that could go there it's perhaps the least egregious one.

[Johan Commelin]

Shreyas Srinivas said:

If anything we in computer science tend to silo ourselves into our niches. We claim that our work helps address grand challenge X(in this case theorem provers for math), and then we measure our research impact not on the application area or end users of X (math/mathematicians), but amongst our fellow researchers (other ITP folks, logicians etc). The former is deemed too practical to be considered worthy of research interest. Lean broke this mould. That is something worth talking about, and as CS researchers, it is something worth learning lessons from.

Slight tangent, but we have the same problems in pure math. All too often, we end up justifying number theory because "cryptography", etc...

[Ruben Van de Velde]

I already had concerns at "definitive account" :)

[Chris Wong]

Shreyas Srinivas said:

Even mathlib borrows several ideas from formalisations in other ITPs.

Notably, the formalization of topology and measure theory is heavily influenced by Isabelle. The filter library is pretty much a direct port.

[Kim Morrison]

Ruben Van de Velde said:

I already had concerns at "definitive account" :)

Isn't this what one might expect from a blurb for a popular science book? This is not the abstract of a paper.

[Shreyas Srinivas]

Another small thing. Looking at the replies to Jon Sterling's thread, the criticism appears to come from a community that carries deep resentment towards the members of the lean community for essentially not incorporating or dealing with their research in exotic foundations. While correcting misinformation and giving credit to researchers is definitely important and necessary, I don't see how it helps to cater to charged criticisms from this community. As Kim says, this is the blurb of a pop science book, not a paper.

EDIT: This comment doesn’t accurately reflect Jon Sterling’s opinions or that of others in the thread. For this is I apologise.

[Ruben Van de Velde]

That seems overly harsh

[Shreyas Srinivas]

I am happy to share specific instances of what I am talking about in DMs, since this is a public channel @Ruben Van de Velde

[Patrick Massot]

@Shreyas Srinivas I think your speculations about the secret motivations of people writing those messages on mastodon are not useful here.

[Shreyas Srinivas]

I was speaking of public posts, but I apologise for that anyway

[David Wärn]

To me, "the 'truth oracle' that thinkers have sought for centuries, a tool to definitively verify or refute any mathematical or logical assertion, no matter how complex" is completely unambiguous. I don't see how it could refer to anything else than the Entscheidungsproblem. Of course we all know that Lean does not solve the Entscheidungsproblem, so we can try to read something else into the sentence. But let's not pretend that the abstract itself says something else.

[Bulhwi Cha]

the “truth oracle” that thinkers have sought for centuries, a tool to definitively verify or refute any mathematical or logical assertion, no matter how complex

I think the writer of the abstract should replace the word "assertion" with "proof."

[Alex Meiburg]

For whatever it's worth, I would not have interpreted that as being about the Entscheidungsproblem, and I don't think there's any age where I would have. (As a 13 year old I didn't know the term "Entscheidungsproblem", but I would still have understood it to mean "verify a proof is true or find a flaw", not "verify that a statement is true or that it's not")

[Mario Carneiro]

Um... The Entscheidungsproblem is literally about deciding statements, not proofs

[Mario Carneiro]

and the description of a 'truth oracle' also seems to be about deciding statements

[Mario Carneiro]

I think it's fair enough to say that this is the holy grail people have been seeking, as long as it is sufficiently clear that lean is not the holy grail

[Mario Carneiro]

people do still wish to have tools that decide statements, not proofs, and much of the tension between ITP and ATP is how much to pretend that we can actually do that vs giving in to the reality and checking proofs instead of statements

[Shreyas Srinivas]

Is it fair to expect a blurb for a pop science book to deal with that level of detail? That being said changing statements to proofs might make it more correct

[Mauricio Collares]

Really looking forward to this book!

[Mauricio Collares]

Also, I think a reasonable interpretation of "truth oracle" is referring to some Lean + AI combination. I know some mastodon posters just dismiss it as "AI pseudoscience", but I find it funny that people would raise such objections when 1) this is possibly the only field where AI outputs can be reliably and automatically checked 2) there is an actual example (AlphaProof) of a system that decides IMO statements, using Lean as a crucial part of the process.

[Alex Meiburg]

Mario Carneiro said:

Um... The Entscheidungsproblem is literally about deciding statements, not proofs

No disagreement there, I'm well aware. I realize my last message had some grammatical ambiguity: when I say that "I would have interpreted it", the "it" was the book abstract

[Mario Carneiro]

the book abstract is clearly about deciding assertions

[Mario Carneiro]

so I'm still confused unless you have an extra 'not' in your first post

[Mario Carneiro]

That is, I'm agreeing with David Wärn 's assessment, the text is unambiguously about the Entscheidungsproblem

[Mario Carneiro]

@Bulhwi Cha if you replace the word "assertion" with "proof" it's no longer about the "'truth oracle' that thinkers have sought for centuries"

[Johan Commelin]

If it is targeted at an audience that has heard of the Entscheidungsproblem, then I would agree.
I am quite sure that the author didn't intend to claim that the abstract was talking about the Entscheidungsproblem, so I think it must have been ambiguous to at least one person.

[Shreyas Srinivas]

An oracle that checks proof and pronounces it correct is a truth oracle

[Mario Carneiro]

?

[Mario Carneiro]

A truth oracle tells you whether things are true, it's right in the name

[Mario Carneiro]

The whole point is that much of the progress in mathematics and logic has been in the search for this holy grail that we now know cannot exist in full generality

[Shreyas Srinivas]

In plain speak, it is not unusual to equate truth to proof

[Shreyas Srinivas]

It is only in math speak that we start being clear about these distinctions

[Mario Carneiro]

truth to existence of a proof, not to the proof itself

[Mario Carneiro]

if you have a proof and the oracle tells you this proof is well formed this is not so oracular of an activity

[Mario Carneiro]

changing statement to proof in that blurb would make it completely wrong

[Alex Meiburg]

I think this is going to be inherently subjective and down to our cultural associations with the words "truth" and "oracle". It's totally fine and reasonable to hear "truth oracle" and read "decides arbitrary propositions". But my point is that this would never have been my first interpretation, at any point in my life, so it's certainly not unambiguously wrong and misleading

[Johan Commelin]

Mario Carneiro said:

if you have a proof and the oracle tells you this proof is well formed this is not so oracular of an activity

That depends on what the first occurrence of "proof" means in your sentence.

[Mario Carneiro]

It is immediately clarified afterward, I don't see how it can be misread

[Mario Carneiro]

the “truth oracle” that thinkers have sought for centuries, a tool to definitively verify or refute any mathematical or logical assertion, no matter how complex.

[Mario Carneiro]

given an assertion, verify or refute it, no matter how complex

[Mario Carneiro]

that's the Entscheidungsproblem

[Edward van de Meent]

so then the question is if "logical assertion" refers to a proof or a statement

[Mario Carneiro]

you don't refute proofs

[Shreyas Srinivas]

Also, although this was not my first interpretation, it can be argued that the author is talking about the much advertised AI + lean combo as @Mauricio Collares pointed out above.

[Alex Meiburg]

Yes, "verify" to me means "verify a claim (which I have a reason to believe, i.e. a proof)". There are many instances in everyday English where "verify" means "verify that some proof is correct", e.g. taxes

[Mario Carneiro]

Verifying a claim generally doesn't come with the presumption that the claimant is providing the verification

[Johan Commelin]

Mario Carneiro said:

you don't refute proofs

That once again depends on the meaning of the word "proof".

[Shreyas Srinivas]

Mario Carneiro said:

you don't refute proofs

Why not? You can refute proof candidates

[Mario Carneiro]

you say something, I check whether it's really true. I am verifying your claim

[Shreyas Srinivas]

And how many people distinguish between proof and proof candidates in plainspeak

[Mario Carneiro]

that's the plain meaning of the term in english

[Mario Carneiro]

so I have to come up with reasons that convince me, you may or may not have supplied them

[Bolton Bailey]

Mario Carneiro said:

Verifying a claim generally doesn't come with the presumption that the claimant is providing the verification

Hmm, I wouldn't say so, I would expect "verifying" a claim to involve checking a provided proof. Wouldn't you say that in the academic review process for a math paper that the reviewers are "verifying" that the paper is correct by checking the proofs?

[Mario Carneiro]

I said not necessarily

[Mario Carneiro]

verification can come with a justification from the claimant but it need not in general

[Johan Commelin]

I am not going to argue that the current phrasing in the abstract is optimal. But I don't agree that it is unambiguously misleading and wrong.
Expecting "proof" to mean "formal proof in the sense of logic" in the abstract of a pos-sci book is ignoring the vast majority of meanings that "proof" has outside of logic.

[Mario Carneiro]

I am arguing that it is unambiguously saying what it is supposed to

[Mario Carneiro]

it is a stretch to read "truth oracle" and interpret it as "proof checker", I think the blurb is using truth oracle to mean truth oracle

[Mario Carneiro]

That sentence is not talking about proof checking

[Shreyas Srinivas]

That’s a matter of interpretation

[Shreyas Srinivas]

You are reading it as a logician

[Mario Carneiro]

no, I am reading the words by their plain meaning

[Mario Carneiro]

People do not use the word "assertion" to mean "justification" in plain language

[Shreyas Srinivas]

[Quoting…]

That’s what I mean. You are reading it with a level of clarity that being a logician gives you

[Bolton Bailey]

Mario Carneiro said:

verification can come with a justification from the claimant but it need not in general

What would be an example of something in mathematics that a verifier would verify without there being an attached proof?

[Mario Carneiro]

An exercise?

[Mario Carneiro]

Usually you would use "prove or disprove" instead of "verify or refute" in a math class

[Mario Carneiro]

for a general english context I would think of something rather like political fact checking

[Mario Carneiro]

an assertion is made, and it is a fact checker's job to verify or refute the assertion

[Bolton Bailey]

Hmm, I suppose I have seen exercises phrased as "verify that a group of this order has this structure". Admittedly I have found that a weird phrasing in the past.

[Mario Carneiro]

in a math context I think there is a slight difference in meaning from "prove": "verify" means "convince yourself" and "prove" means "write something that would convince me"

[Bolton Bailey]

Well, in the context of exercises, the point for me has always been for me to convince the professor I understand the material! Maybe there are people who do exercises for fun and not because they are part of a problem set.

[Mario Carneiro]

I think that's why you won't see "verify" in exercises much

[Mario Carneiro]

Anyway, my point is that while the "truth oracle" sentence is fine, the following sentence strongly implies that lean is a truth oracle, or at least doesn't care to clarify on the ways it is not the magical tool that solves all problems

[Jireh Loreaux]

I don't even think the "truth oracle" sentence is acceptable. The precursor is:

... a small group of mathematicians recognized [Lean's] potential to become something far more powerful: the "truth oracle" that thinkers have sought ...

[Mario Carneiro]

that's true, the "truth oracle" can only really be described as a guiding star or otherwise influence on ideas for tools, it's not literally a thing that exists

[Mario Carneiro]

I think you could probably use the same words to describe GPT

[Shreyas Srinivas]

If someone described ChatGPT like that in a pop science book, I wouldn’t object to it. There is some literary license to write in a flamboyant way in such books.

[Bolton Bailey]

Anyway, to summarize my thoughts, I see six possibilities:

1. The blurb author meant to say that the Lean community thinks Lean will solve the Entsheidungsproblem, in which case they are mistaken, because we are familiar with Gödel's incompleteness theorem.
2. The blurb author did not mean to say that the Lean community thinks Lean will solve the Entsheidungsproblem, but rather to speculate that Lean will have some sort of AI that can find proofs as well as any human, in which case they probably shouldn't have used the phrase "no matter how complex".
3. The blurb author meant to say that the Lean community thinks Lean has the potential to mechanically check proofs, in which case they not exactly wrong. But they are wrong in that Lean and all other ITPs already do this by their very nature, and so it's not right to say that Lean was "originally conceived" as something else.
4. The blurb author thinks or feels that all these things exist on some kind of imprecisely-specified spectrum and doesn't mind using the phrase "truth oracle" to represent all parts of that spectrum at once. In which case, they are being pretty vibey in a "not even wrong" sort of way.
5. The blurb author takes the esoteric philosophical view that truth and provability are the same thing, and that Lean can prove all true statements by enumerating all proofs, even though it would take arbitrarily long amounts of time.
6. The blurb author doesn't really understand these concepts and is just trying to summarize the book in a way that sounds cool.

Truly though, I feel none of these rise to "fuck Quanta" levels of public repudiation.

[Rob Lewis]

As an expert writing for a non-expert audience, there's a strong expectation that you don't mislead. Think from the perspective of someone who doesn't already know what a proof assistant does or what the Entscheidungsproblem is: "the “truth oracle” that thinkers have sought for centuries, a tool to definitively verify or refute any mathematical or logical assertion, no matter how complex" is clearly going to tell you whether a statement is true or false. It's not poetic license, it's misleading. "The most upsetting I've ever read" is pretty rich but I do hope this blurb gets changed.

[Bolton Bailey]

Well part of what I am suggesting is that I'm not sure the person who wrote this is an expert.

[Shreyas Srinivas]

Bolton Bailey said:

Truly though, I feel none of these rise to "fuck Quanta" levels of public repudiation.

Agreed. Neither does it merit claims about some projects getting too much attention.

[Jireh Loreaux]

Well, if they aren't, then they should at least be consulting experts about this blurb.

[Jireh Loreaux]

Honestly, if this sentence isn't supposed to mean what it purports, and instead it is supposed to mean "Lean is a proof verifier", then this is just a (bad) recapitulation of something stated in the first sentence: "... Lean, a proof assistant ..."

If I were rewriting this, while trying to retain as much of the original as possible, but also giving credit where it's due and being accurate, I would write something like:

THE PROOF IN THE CODE is the definitive account of the birth and rise of Lean, a proof assistant initially developed at Microsoft that is transforming the enterprise of mathematics and ushering in a new era of human-computer collaboration. Although Lean was originally conceived as a tool for verifiying correctness of programs, a small group of mathematicians recognized it can also be used as a proof assistant --- a tool to verify mathematical proofs. Such tools have existed for decades, and Lean builds upon those years of insight, but Lean's particular feature set took the mathematical world by storm in a way that previous proof assistants did not. This is the story of a grassroots effort to bring Lean into mainstream programming and forever change the interaction between mathematicians and computers. Filled with insights about the future of math, computers, and AI, THE PROOF IN THE CODE is a brilliant work of journalism by Kevin Hartnett, a leading math writer whose research and reporting offer a profound answer to a longstanding mystery: Can computers reveal universal truths?

In the above, I've attempted to remedy many of the issues with the original:

1. Lean was initially developed at Microsoft. I think by is also reasonable here, but Lean is no longer developed there.
2. It retains the "originally conceived as a tool for verifying correctness of programs", because, from what I can tell, that is accurate (although Leo knew it could also be used for mathematics).
3. This makes clear that Lean is a proof assistant, just explaining the claim in the first sentence, and it does not claim to solve the Entscheidungsproblem.
4. It makes clear that it is not the first, and pays homage to those that came before.
5. It emphasizes one of the key points about the Lean / mathematician interaction: not that Lean was the first to fill this role, but that it had much greater appeal to mathematicians than other proof assistants.
6. It tries to still to flamboyant (e.g., "took the mathematical world by storm") to appeal to the reader.

Is the above perfect? Perhaps not, but I think it proves it's possible to complete the task without making wild claims that are, if not unambiguously, at least easily interpreted as Lean solving the Entscheidungsproblem, and (hopefully) without pissing off users of other proof assistants.

[Alex Kontorovich]

I'm on the Scientific Advisory Board at Quanta (the magazine, not the new book series which prompted this discussion...). Once the dust settles here, if you think there is some useful feedback that could go back to their editors/writers, please let me know and I'll be happy to pass it along. (If you think it's easy to write for the public, saying things in such a way that lay people will learn something, but without upsetting experts who know the myriad ways one has to lie to succeed at the former... well, then I guess you've never tried writing for the public...)

[Alex Kontorovich]

(I've been on numerous email threads of experts similarly dissecting various Quanta articles over the years. Hence the appeal on my website: "If you have a complaint about an article, please send it to the other mathematician on the Board, Laura DeMarco" :smile:...)

[Frederick Pu]

I think as long as it's emphasized that it's the proofs that are being checked and not the statements themselves, the theorem proving aspect will be factually authentic. And then in terms of not giving all the credit towards lean, the main point should be that lean brings together a lot more mathematicians.

[Kim Morrison]

(Perhaps worth noting that we would like to be checking statements too --- of course not universally --- currently plausible is barely usable, but I'm hopeful this will change and we'll get to a future where as soon as you type :=, any easy counterexamples are shown in the InfoView.)

[Shreyas Srinivas]

Update: I had a chat with Jon Sterling. It was a healthy exchange about my message above, about his thread. I realised that I ended up misrepresenting his position and for that I unreservedly apologise again.

We discussed the replies to his mastodon thread and this Zulip thread, as well as the general state of affairs about the discussion of proof assistants history and its presentation in the press. He proposed that there should be a joint effort in the form of a position paper or editorial to clarify the history and current status of proof assistants and what they can or cannot do, and I personally agree that this would be a good step forward.

[David Michael Roberts]

A Quanta article about the history of proof assistants and how they take different approaches, but also learn from each other, would be a good read and a useful 'soft' reference, if done well. Of course, an actual detailed survey paper aimed at experts would be good, too, but in the current AI-is-magic environment, especially with things like proof assistants feeding into AI-winning-at-math!!1! (when given problems/solutions in advance?), having a mass-audience article might be better. Certainly to inform people who might be investing money in companies that want to treat the proof assistant+LLM as some kind of woo-woo that will somehow give us AGI