merging formalization into the original paper

Stream: general

[D. J. Bernstein]

Right now there's a common two-stage process of (S1) a paper presenting theorems followed by (S2) a subsequent formalization paper using some proof assistant to present computer-checked proofs. I've been doing a literature search with the goal of finding (S12) papers that merge these two stages: the computer-checked proofs aren't a subsequent paper but are already in the original paper. The interesting corner case of proofs that were found by a computer in the first place is easy to find, but I'm looking for non-automated examples.

A search that names any of the popular proof assistants is flooded with examples of S2, and I haven't figured out how to narrow this in a way that finds S12. I haven't even figured out how searches would find my own S12 papers, or https://www.cl.cam.ac.uk/~jrh13/papers/holhol.html and its followups, without using pre-knowledge of those papers.

Has anyone seen names for the S2/S12 distinction? (I've tried various names that produce no search results; the most comprehensible names I've thought of so far are "papers _on_ computer-checked proofs" vs. "papers _with_ computer-checked proofs", but there's no reason that a paper of the second type would use that terminology.) Does anyone have a list of S12 papers, or individual examples?

I did notice https://xenaproject.wordpress.com/2023/01/08/lean-2022-round-up/ saying that Mehta and Bloom finished a "full formalisation of Bloom’s result" before "Bloom had received a referee’s report for the paper", but it isn't clear to me whether formalization here refers to the proofs or just the theorem statements. Also, this example doesn't sound like it has the basic S12 advantage of reducing the referee's proof-checking load.

[Alex J. Best]

Mehta and Bloom did a full formalization including all proofs down to leans standard axioms (building on mathlib). It is of course unlikely that the referees know lean (but not impossible) though it may have helped convince someone they didn't need to check every last detail. I guess only @Thomas Bloom can say for sure if they heard anything to that effect from the referees/ editor at any point?

[Thomas Bloom]

Yes, everything including all proofs was formalized. The referee's report was received after the formalisation was completed (and publicly announced), and did not mention Lean or the formalisation, so I don't know whether the referee was aware of it.

[Thomas Bloom]

After the referee's report was received I let the editor know about the formalisation, and an appendix has been added to the original paper describing this.

[Eric Wieser]

I'm in a the process of publishing a paper where every result mentioned within the paper is annotated with a link to the formalization, though the paper itself barely mentions formalization

[Jannis Limperg]

In programming language research (conferences: POPL, PLDI, ICFP) S12 papers are very common. If you look at papers accepted at these conferences, you'll find many examples.

[Johan Commelin]

Besides the unit-fractions project, the only example I can think of is @Neil Strickland's https://arxiv.org/abs/1907.07801.

In general, I think S12 is very rare in maths, simply because the boundary of what can be formalized is often quite far from the boundary of research-level maths.

[D. J. Bernstein]

Thanks for the pointers so far! My objective here is to cite a reasonable spread of examples that a skeptical reader can spot-check, so the level of documentation is important: e.g., even if https://arxiv.org/abs/2112.03726 will end up qualifying as S12, right now it's just the 2021 version.

[D. J. Bernstein]

And, to be clear, the scope I'm interested in includes any paper that states a theorem; I'm not trying to draw lines between math and CS.

[Oliver Nash]

With apologies for citing my own work, as far as I'm aware, the main result of this paper (see section 4) did not previously appear in the literature: https://link.springer.com/article/10.1007/s10817-023-09668-0 (and indeed I found it a bit hard to believe until I had formalised it).

[Adam Topaz]

The closest one of my papers comes to (S12) can be found here: https://raw.githubusercontent.com/adamtopaz/CoeffAltPairs/main/main.pdf
But I still have not submitted this anywhere, so I don't have any idea what a generic referee might say.

[David Ang]

Our paper has a new proof on the group law on Weierstrass curves that afaik isn't anywhere in the published literature, but I guess that's not really a new theorem

[D. J. Bernstein]

Preprint examples are great. de Bruijn commented in 1991 on the goal to "lighten the burden of referees of mathematical papers"; clearly this is most effective if the formalization is there before refereeing begins.

[Thomas Bloom]

D. J. Bernstein said:

even if https://arxiv.org/abs/2112.03726 will end up qualifying as S12, right now it's just the 2021 version.

I'll update the arxiv version with the new appendix about the formalisation later this week.

[D. J. Bernstein]

Great!

[Martin Dvořák]

I was thinking about this topic a lot in the past. Sometimes I was thinking out "loud" like here:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Publishability.20of.20novel.20research

Since then, my opinions have shifted a bit in the following direction:
If you can publish two papers, why wouldn't you want to?
If you do S1 in area where S2 is feasible, why don't you first publish S1 and subsequently S2 elsewhere?
I am not saying it is better for science (arguably, doing S12 together would be better overall) but it is better for you personally -- publications are our currency -- two publications are more than one publication.

Maybe you solved a problem where S1 was too easy to impress reviewers by S1 alone, so you do S12 together and bring S12 to a formalization conference? I am saying "S12 to a formalization conference" because I am worried that, in situation where S1 would be seen as too easy, S12 would not convince "math reviewers" either. But I'll be happy if you prove me wrong!

[Sebastien Gouezel]

I have two S12 papers, see https://perso.univ-rennes1.fr/sebastien.gouezel/articles/SubMult.pdf (especially Remark 1.3 there) and https://perso.univ-rennes1.fr/sebastien.gouezel/articles/morse_lemma.pdf (in the latter paper, the preprint version had more details on the formalization, but the referee asked us to remove it as it was not interesting at all in his own view...)

[Martin Dvořák]

I think there is a spectrum between S2 and S12. If you make an ITP paper about a folklore theorem (like I did), I think it falls somewhere in between S2 and S12.

[D. J. Bernstein]

I'm interested in hearing about examples in the gray areas too.