Paul Boes

Stream: new members

[Paul Boes]

Hi all, I'm a theoretical physicist, having recently finished my PhD in quantum information theory, with a particular focus on thermodynamics/statistical mechanics and generalized entropies/the theory of majorization (@Frédéric Dupuis and @Jalex Stark are two names here whose work is relatively close to mine). I also have an academic background in philosophy of science/physics and economics.

I'm here because I'm worried about a "replication crisis" in my field. For my own "proofs" I have utilized all kinds of statements whose proof I didn't check/couldn't fully understand and peer reviewers didn't spot mistakes that I had made in my derivations. I'm not sure about the extent of this problem in different fields and the damage it incurs (there are several dynamics that should lead to a quick identification of errors in published results), but I'm intrigued by the possibility of "simply" attaching executable proofs in Lean to papers to reduce the chance of erroneous research being dispersed.
I'm not sure where on this forum members discussing the above gather and would be thankful about any pointers. Also happy to start a new topic/stream about more general meta-science topics.

[Scott Morrison]

We haven't had too many discussion here about the replication crisis per se, although it's certainly something that lots of us have thought about. Kevin Buzzard (formerly a famous number theorist, now active here :-) has given a number of thought- (and controversy-!) provoking talks about it the idea of a replication crisis in pure mathematics, and you can find his talks on youtube.

[Scott Morrison]

But I think a lot of people here are at least as interested in other motivations for interactive theorem provers:

• the prospect of gaining superpowers by doing mathematics with a computer as an assistant
• pedagogy, and teaching proofs to undergraduates
• a playground for machine learning research

[Kevin Buzzard]

I think that in pure mathematics most people are completely unconcerned with the replication crisis to the extent that I have basically stopped going on about it now.

[Jalex Stark]

I think us CS theory / physics folks have a worse replication crisis than the pure maths folks because, well, our people and our publication venues are just less skilled at proof-checking. I gave a talk at QIP 2018 where the main theorem was false. The error could be spotted as early as page 1 of the preprint, where I made a claim whose counterexample could be checked by multiplying some 9x9 matrices together in sage.

[Frédéric Dupuis]

Welcome! It's always nice to see a fellow quantum information theorist here.

I think in our field the problem might be bigger than in pure math, because of the different publication culture. On the CS side of the field, most results end up published as conference proceedings and not journal papers, which means that reviewers are working on tight deadlines, so if there's a mistake in say, Lemma 37 in Appendix B, the odds that it will be caught be a reviewer are pretty low. On the physics side, the most prestigious journals (Nature and friends) tend to put a lot of emphasis on marketing the result, and with more mathematical papers the main part of the text ends up being some sort of advertisement for the real thing which is relegated to the "supplementary material" that doesn't seem to be as carefully read by reviewers. Other journals like Physical Review Letters have extremely short page limits which also encourages corner-cutting.

[Frédéric Dupuis]

Right -- it can also happen with Theorem 1 on page 1 :-)

[Jalex Stark]

I'll agree with Frédéric's point, too. I recently got a paper through nature communications, and I don't feel any more confident that it's bug-free now than before we submitted. It just didn't seem like that's what we were being evaluated on.

[Frédéric Dupuis]

Yeah, papers are mostly evaluated on their importance and novelty. Officially also on correctness, but reviewers just don't have the time to do it properly. For a conference like QIP, PC members have something like 20 papers to evaluate in about one month. Some of that work can be delegated to subreviewers, but this is still a very tight deadline.

[Jalex Stark]

I'm pretty sure the most efficient path to "just attaching verifications" to results in quantum information theory is

• get probability theory and finite-dimensional hilbert spaces into mathlib
• write a document that looks like the "preliminaries" section of a good paper, where the proofs are all "apply a special case of something that's in mathlib".
• state some of your colleagues' results in Lean, show them the statements + your preliminaries, convince them to take a stab at filling in some sorrys.

[Jalex Stark]

I think this is similar to Frédéric's current approach (at least, they've made some progress on the first bullet point), though I don't want to put words in their mouth.

[Frédéric Dupuis]

I agree! In fact I think the "just do it" approach has a decent chance of working: once we're through with the first bullet point, it will become possible to formalize at least parts of the papers that we publish (i.e. self-contained lemmas, that sort of thing). Then, we can just start including them in our papers when submitting. And then you gain an advantage in the reviewing process: the paper instantly looks more credible and the reviewer has less work to do. Hopefully that will make readers curious and we'll see some of them appear here.

[Wrenna Robson]

I'm still quite new to cryptography but some of these issues are sounding remarkably similar in that context too...

[Wrenna Robson]

Certainly I have literally heard conversations essentially along the lines of "what is the purpose of provable security if nobody reads the proofs".

[Paul Boes]

Thanks everybody for your replies.
I agree with your reasons, Jalex and Frédéric, for why quantum info (and other more applied fields) might suffer from more of a replication crisis than than pure mathematics. At the same time, I believe that the bottom-line reaction by people in the community might be the same - lack of concern - but for different reasons: While physicists are less-skilled at proof checking, the demands on proofs are also lower. Most of the errors in proofs might never actually do any harm, since where they go wrong is not where physicists care for them to be correct, etc. I am also not aware of a major castle of sand having been burst and pulling a large chunk of papers down with it, the kind of incidence that could be used to motivate people to invest the time into coding up their proofs and attach them to their papers (I'm currently preparing a survey to be send around, where I want to get some feedback on this).

This makes me believe that the possibility of a crisis itself may not be the most compelling argument for attention towards Lean et al. Potentially it would be better to focus on the notion of a search engine: "Does there exists a theorem in the literature that shows something similar to X?" (where X is a Lean statement). This is because a database of published theorems could be filled without the proof - just the statements of the asserted theorems. Collecting those statements in crowd-sourced fashion (maybe in form of a Preliminary doc accompanying the paper, as suggested by Jalex) could be significantly easier than getting people to write up the proofs. Then, once people use the search engine, they'll (hopefully) want to know whether a theorem actually holds, etc. I'm suggesting this being fully ignorant about how a useful search engine based off of Lean statements could be built.

In that sense, while the "just do it"approach might have a chance of working, running additional strategies alongside (such as guessing theorem statements from their latex and then proactively asking authors to confirm the guess/modify it to populate a database that forms the basis of a search engine) might be viable as well. Obviously, already for this much simpler strategy, the first bullet point would have to be taken care of.

Finally, as an additional note: I think another difference from applied fields to pure mathematics is that in the former the real value of prover systems could be in the "long tail" of theorems and lemmata that don't really show anything genuinely novel or original but rather apply a general theorem to a special case or generalize existing knowledge by an epsilon: Such proofs could be quite simple to code up in Lean, since they mostly rely on very basic building blocks, but they'd prevent the accumulation of many small errors, leading to cheap confidence. This seems to be very different from pure math, where maybe the long tail is much shorter/there's more confidence in that tail not containing errors?!

[Yury G. Kudryashov]

For me one of the reasons to start looking at Coq, then at Lean was a week when I found mistakes in 3 papers I wanted to use: one had a typo in a non-essential lemma (I wanted to cite this lemma, had to prove a correct version instead), one paper claimed a result for n≥2 but the proof for n=2 was wrong, and one had a hole I still don't know how to fix (though now I have a simpler proof of the theorem). Another reason was a hole in my own master's thesis.

[Jalex Stark]

I guess the idea of formalizing just the abstracts of papers so you can make a search engine has been considered by thomas hales, but they haven't gotten very far in terms of public-facing work.

[Jalex Stark]

We talk about writing more "formal roadmaps" around here sometimes, this is a scaled down version of the same idea.

[Jalex Stark]

The issue is that you have to be really confident in your ability to write good definitions in order to write a good formalization of just the statements without the proofs. If your definitions are extensible, play well with each other, and minimize the trivial inconveniences for proving stuff about them, they'll see use. If they're not, they won't.

[Jalex Stark]

In 2020, contributing directly to mathlib is probably the most efficient way to become very skilled at writing formal definitions.

[Frédéric Dupuis]

I have to say I'm a bit puzzled by this notion of having a database of formalized statements. It seems to me that to be able to state the theorems, you need the big pile of definitions that they rely on to be formalized, and once that is done, the actual proofs cannot be very far behind. Figuring out the structure of the library seems to be the tough part in what we're doing here, the actual proofs are much easier.

[Kevin Buzzard]

"the actual proofs cannot be very far behind" -- this is nowhere near the truth in advanced mathematics.

[Ruben Van de Velde]

I supposed Jalex was referring to https://formalabstracts.github.io/

[Frédéric Dupuis]

@Kevin Buzzard Yeah, maybe I went a bit far here -- of course you have things like Fermat's last theorem where the statement doesn't refer to the definitions that are relevant in the proof. But at least in the areas I work in, those statements feel very much like the exception rather than the rule.

[Kevin Buzzard]

Yes, I've seen stabs at both modular forms and elliptic curves in Lean, but we knew what these things were 50 years before we proved FLT using them.

[Wrenna Robson]

Out of interest (just because this is the area of maths I care about) what are the challenges to defining elliptic curves? Or is it more that it is just simply a large amount of work to do and nobody's done it yet?

[Alex J. Best]

The challenge is the group law. Depending on what generality one works in there end up being a lot of pretty huge algebraic identities to verify to show it is well defined and associative. I think Kevin and John Cremona got a version defined at lean for the curious mathematician a couple of months back for a bit of fun.

[Kevin Buzzard]

We defined the group law, but it took a long time because the equations are too long to be easily manipulated in Lean

[Alex J. Best]

One thing that would really help is a better infrastructure for verifying these identities aka having grobner bases in lean so that's a sort of sticking point. But we could definitely add some definition of elliptic curves and define the j invariant and discriminant and stuff without any of that.

[Kevin Buzzard]

We used Groebner bases when defining addition. We wanted to take short cuts with the algebra to bring it down to a reasonable size so John did some Groebner basis calculations in sage and we copied and pasted the results into our proof.

[Wrenna Robson]

I'm assuming that e.g. defining isogenies would have similar issues in terms of the scale of large algebra.

[Johan Commelin]

Unless you do it properly, and define an elliptic curve to be a scheme ... etc ...

[Johan Commelin]

Then you don't need to manipulate any equations

[Alex J. Best]

Yes but we are some way from the picard group and things it seems!

[Kevin Buzzard]

We're not far from the Picard group of a ring, and we're making progress on schemes. We'll get there in the end :-)

[Bassem Safieldeen]

Paul Boes said:

Hi all, I'm a theoretical physicist, having recently finished my PhD in quantum information theory, with a particular focus on thermodynamics/statistical mechanics and generalized entropies/the theory of majorization (Frédéric Dupuis and Jalex Stark are two names here whose work is relatively close to mine). I also have an academic background in philosophy of science/physics and economics.

I'm here because I'm worried about a "replication crisis" in my field. For my own "proofs" I have utilized all kinds of statements whose proof I didn't check/couldn't fully understand and peer reviewers didn't spot mistakes that I had made in my derivations. I'm not sure about the extent of this problem in different fields and the damage it incurs (there are several dynamics that should lead to a quick identification of errors in published results), but I'm intrigued by the possibility of "simply" attaching executable proofs in Lean to papers to reduce the chance of erroneous research being dispersed.
I'm not sure where on this forum members discussing the above gather and would be thankful about any pointers. Also happy to start a new topic/stream about more general meta-science topics.

Hi @Paul Boes !

If you ever think about building a quantum information theory Lean library and find yourself in need of an extra pair of hands please let me know! I am interested in quantum information theory, and am trying to build a Lean library up enough to start working on research questions.

[Jalex Stark]

@Bassem Safieldeen, I think the beginnings of the quantum info library are the recent PRs by Frédéric to mathlib. If you want to be handy, that's probably the right place to chip in.

[Bassem Safieldeen]

Will check them out, thanks!

[Frédéric Dupuis]

Welcome aboard, @Bassem Safieldeen ! Indeed I'm interested in getting mathlib to the point where current research in quantum information can be formalized. To give you an idea of where we are at right now, we are now in process of merging complex inner product spaces (#4057) and eigenvalues/vectors (#4111 and several other PRs by Alexander Bentkamp). The next step would be to get the spectral theorem based on these, and then start doing Hermitian operators, unitaries, and so on. So for the time being at least, it doesn't really make sense to do things that are specific to quantum information, we're still formalizing the basic math needed to get started.

[Bassem Safieldeen]

Awesome! I will try to help!

[Paul Boes]

Thanks @Bassem Safieldeen , will definitely do (although right now it seems very unlikely). I think you've received the most promising pointers already :)