Publishability of novel research

Stream: general

[Martin Dvořák]

[soft question]
Can novel mathematical research be published at conferences such as ITP?

Let's say I discover a new property of some algebras.
It is novel but it the proof was not difficult enough for mathematical journals to be willing to publish such a paper.
Can I formalize it and submit the (informal) pdf describing the proof to a conference such as ITP?

Would it be OK ethically?
And would it be viable practically? (that ITP might actually publish such a paper)

[Oliver Nash]

I have not published in ITP and cannot answer your question but I think that https://www.springer.com/journal/10817 is potentially a good home for such work (ableit sadly not open access).

[Martin Dvořák]

Have there been papers of this kind in JAR before?

[Martin Dvořák]

Or is there any indication they would want such papers?

[Martin Dvořák]

I should have said that I was asking more generally. I cannot submit to JAR — for a simple reason — my advisor is the chief editor. Is there any journal or conference where submitting such work would be viable?

[Jannis Limperg]

You can still submit to JAR. Jasmin will just recuse himself from any activities involving your paper. If you're unsure whether a paper is a good fit for JAR, ask Jasmin.

[Martin Dvořák]

Really? Even if he were a coäuthor?

[Jannis Limperg]

In that case probably no, but just ask him.

[Jason Rute]

Jeremy Avigad (my advisor) and I once submitted a paper to the journal of Logic and Analysis of which he was an editor. We let the other editor handle every part of the process. But I’m sure different people have different feelings on this sort of thing and different journals have different rules.

[Martin Dvořák]

Or better, I can choose a different journal, without a conflict of interest.

[Jireh Loreaux]

"Better" may depend on whether or not there is another journal which is just as suitable for publication. Sometimes there's only one ideal journal.

[Jireh Loreaux]

For example, Jasmin just published "superposition for HOL" in JAR, but I wouldn't say that was a bad choice because the topic is closely aligned with the journal's scope.

[Martin Dvořák]

Jireh Loreaux said:

"Better" may depend on whether or not there is another journal which is just as suitable for publication. Sometimes there's only one ideal journal.

Good point! Are there any other venues (apart from ITP and JAR) for publishing formal proofs that were not written in Mizar?

[Martin Dvořák]

Jireh Loreaux said:

For example, Jasmin just published "superposition for HOL" in JAR, but I wouldn't say that was a bad choice because the topic is closely aligned with the journal's scope.

It seems to me that the paper you mentioned was published in JAR but not reviewed by JAR. They say it is a part of a collection "Selected Extended Papers of CADE 2021".
https://link.springer.com/collections/gadbadhdfa

[Martin Dvořák]

Martin Dvořák said:

Are there any other venues (apart from ITP and JAR) for publishing formal proofs that were not written in Mizar?

I am still interested in this issue. Apart from ITP and JAR, are there any journals or conferences that publish formal proofs not written in Mizar?

[Kevin Buzzard]

Yes -- for example Exp Math (a journal) and CPP (a conference proceedings).

[Martin Dvořák]

https://www.tandfonline.com/journals/uexm20

[Martin Dvořák]

https://popl18.sigplan.org/series/CPP

[Kevin Buzzard]

Exp Math only recently got into formal proofs -- search e.g. formalizing to see some examples. @Alex Kontorovich should be able to say whether Exp Math is still interested in formalisations of mathematics (he's the managing editor of the journal).

[Alex Kontorovich]

Well, just FYI, the entire editorial board and I resigned a few months ago from Exp Math...

[Martin Dvořák]

Will the journal continue without you?

[Kevin Buzzard]

Alex Kontorovich said:

Well, just FYI, the entire editorial board and I resigned a few months ago from Exp Math...

Not according to https://www.tandfonline.com/action/journalInformation?show=editorialBoard&journalCode=uexm20 !

[Oliver Nash]

Perhaps somebody who understands a bit about this could add a remark about it here: https://en.wikipedia.org/wiki/Experimental_Mathematics_(journal)

[Moritz Doll]

Martin Dvořák said:

Will the journal continue without you?

The more important question is whether the editorial board plans on founding a new journal (hopefully without a commercial publisher)

[Martin Dvořák]

Did the editorial board resign because they didn't agree with publisher's requirements?

[Adam Topaz]

Coming back to this topic... perhaps it would be worthwhile to compile some sort of list (probably on the lean community webpage) of journals that are friendly (whatever that means) to formalized mathematics. This might be especially important now given the news about exp. math. above, and the fact that the other two journals listed on the wiki page that Oliver mentioned (J. Algebra's computational algebra and the LMS J. of computation and mathematics) seem to be dead as well.

[Matthew Ballard]

Sounds like @Kevin Buzzard should start a journal :wink:

[Matthew Ballard]

(Notice the winky face!)

[Kevin Buzzard]

Believe me this has been discussed, but the main problem with that is that Kevin Buzzard spent two hours during a boring meeting today not paying any attention and reading, for the first time, emails which had been sent to him in mid-February. A consequence of this is that he now has under 1500 unread emails which is a 2023 record. This is not someone who should be organising anything important :-/

[Johan Commelin]

Suggested name of the journal: "Formal proofs, by friends, for friends" :wink:

[Kevin Buzzard]

Yeah that's the other problem, Kevin Buzzard's journal featuring lots of publications by Kevin Buzzard's mates is not a good look

[Moritz Doll]

If I remember correctly, there was also the question on whether journals are the appropriate way to publish formalized mathematics (I think we discussed that Johan and some other people at ICERM). I did not bother with trying to write an article about formalization, because I'd rather formalize more mathematics, than do some write-up (or rather port stuff to Lean 4).

[David Loeffler]

I did not bother with trying to write an article about formalization, because I'd rather formalize more mathematics, than do some write-up (or rather port stuff to Lean 4).

I think this is not a problem specific to formalization. Most mathematicians enjoy doing new mathematics more than they enjoy writing up the stuff we've already done; but if you don't have journal publications, you won't get an academic job.

[Moritz Doll]

I agree with the statement about doing mathematics being more enjoyable than writing up the results. However, I would think that most mathematicians consider publishing articles worth the time (if people write articles not for the sake of research but to bolster their cv, then this is an issue imo, but this is another discussion).
On the other hand, if you formalize (say) the definition of the Fourier transform and encounter a few pitfalls along the way, does that warrant a paper? It is a very important thing to do and you should get credit for that, but I doubt that a separate publication has too much value. This is not to say that there are no good articles to be written about formalizing mathematics.
Arguably the act of getting mathematics into mathlib is already a form of publication and the deviations can better be documented in the module descriptions or the theory docs.

[Martin Dvořák]

I agree with you both @Moritz Doll @David Loeffler guys!

[Kevin Buzzard]

I think that if you try and formalise Fourier transform and encounter a few pitfalls along the way then this is exactly the sort of thing that the traditional routes such as ITP and CPP and CICM want to hear about. I would also argue that if you formalise some hard modern mathematics and you don't encounter any pitfalls then there's also an argument for publishing because you will have inevitably have organised the material into some kind of coherent form or abstraction which might not be available in the literature. I learnt this way back in the perfectoid days when Patrick was trying to understand extending continuous maps along injections with dense image and at one point just dropped injectivity and realised what was actually going on (he wrote it up in the paper). Groups with zero are another example. I think these things are worth recording in some way other than <URL to some GitHub page containing some code> which most people will never read or understand without a coherent human-written explanation.

[David Loeffler]

@Moritz Doll

If people write articles not for the sake of research but to bolster their cv, then this is an issue imo, but this is another discussion.

"Oh, you poor sweet summer child"...

Journal publications long ago ceased to serve any purpose whatsoever in the dissemination of research. The Arxiv does that. Do you know how long it takes for a serious research article to be refereed these days? I've known delays of two years or more. By the time an article gets published, the vast majority of the people in the world who are going to read it have long ago done so.

Arguably the act of getting mathematics into mathlib is already a form of publication and the deviations can better be documented in the module descriptions or the theory docs.

It would be nice if the world worked that way; but, sadly, mathlib PR's won't get you a job.

(edit: I @ tagged the wrong person for the quote, sorry!)

[Arthur Paulino]

I am not an academic, partially because of some aspects shown in this thread. This is nothing new under the sun, but my impression is that the dynamics of society have changed a lot in the past 30 years due to the internet and the academia is still lagging behind. The reward/punishment system feels outdated to me.

[Martin Dvořák]

Since I want to get a job in academia, I am also guilty of focusing too much on getting peer-reviewed publications.
Honestly, writing up formalization papers is much less fun than the actual work.

Ideally, I would like formal proofs accompanied by a peer-reviewed abstract to count as an "official" publication for our CVs.
The peer review (which needs to check only the definitions, the top-level theorems, and the abstract) would serve for establishing that the code is correctly aligned to the informal notions (the results claimed in the abstract).
Nobody needs to read the rest of the code; the compiler does.

Seems I have just reïnvented https://fm.mizar.org/ ooooops!

[Kevin Buzzard]

There's also Isabelle's AFP, which is similar.

[Martin Dvořák]

I have just realized that AFP has ISSN as well!

[Sam van G]

Just to add a positive data point to what was already said by @Kevin Buzzard above: I do think it is important to also write up formalization results, not for the CV, but for science!
Together with a co-author I recently published my first article on formalization ever, a write-up of our formalization of a relatively niche but non-trivial theorem from mathematical logic from the 1990s. A few months later, this article has already led to significantly more immediate reactions and new research interactions than the average “article with sparkling new theorems” but without formalization aspect that I normally post on Arxiv and submit to a regular math journal. This might of course also be thanks to other factors than just the fact of having formalized the result but I don’t think it’s entirely unrelated.
This experience so far at least shows me that a careful write-up of a formalization of a known but non-trivial theorem, in which you explain the unexpected turns and insights that occur unavoidably when you formalize a paper proof, has real research value that goes beyond just “improving the CV” or “spreading the gospel of proof assistants”. Incidentally, for me personally these two are not the most useful motivating factors to keep me going with formalization, whereas new collaborations and interactions with others interested in the same math topics as me definitely are! (It is always a shame to me if researchers leave academia just because they got the impression that writing articles is only a bureaucratic and/or self-promotional activity, but that is a longer and different discussion.)
The reactions we received on our article were more related to how we proved the theorem than to the formalization aspect itself, even if our formalized proof closely resembles the original one, it was considered difficult and not very well understood (although there was no doubt about its correctness) and our formalization helped clarify some aspects of the proof. Researchers interested in the details of the proof picked up on some changes and clarifications that we had to make because we formalized it. Finally, I recently met for the first time the original author of the pen-and-paper proof that we formalized, and he was very positive about our work.
In summary, I think without the accompanying write-up & publication, our formalization might have gone completely unnoticed, and I consider it a necessary and enriching part of the formalization process.

[Ruben Van de Velde]

You can't just say that and not link to the article :)

[Sam van G]

Ruben Van de Velde said:

You can't just say that and not link to the article :)

I didn't want to become guilty of the very self-promotion that I was saying in the same post was not the point of writing articles, but since you asked: it's here.

[Martin Dvořák]

Sam van G said:

I do think it is important to also write up formalization results, not for the CV, but for science! (...)

I want to second that!
Formalization can indeed find&fill gaps in existing knowledge, even if nobody has been suspicious of it.

A few months ago, I formally proved a theorem that sounds nearly trivial:
"Grammars are closed under the Kleene star."
I think it is a prime example of what is called a folklore theorem. Almost every computer scientist knows it is true but nobody published its proof.
Proving it turned out to not be as easy as I thought. Informal description starts on page 10 here:
https://arxiv.org/pdf/2302.06420.pdf
My proof hasn't gotten any reaction at all. Maybe it will come later. Now it is in review for ITP. The point I am making is that, without formally proving the theorem, I would never care to develop the informal proof and write it down. And possibly nobody would.

On the other hand, formalization papers also make me a bit sad. Towards the future, I don't like the idea that a Lean code accompanies a piece of MathematiCS. My dream is that the Lean code is the MathematiCS. And, since formalization papers treat the Lean code as a supplementary material (as opposed to being the main thing), they keep anchoring us to the state when the Lean code merely accompanies a piece of MathematiCS. I dream of a future when Lean in the language in which we do MathematiCS, from the first sketch of a new idea. Right now, Lean looks like a foreign language into which we translate our MathematiCS. I want Lean to be our native language for all MathematiCS.

[Martin Dvořák]

Ruben Van de Velde said:

You can't just say that and not link to the article :)

image.png

[Bulhwi Cha]

Martin Dvořák said:

I dream of a future when Lean in the language in which we do MathematiCS, from the first sketch of a new idea. Right now, Lean looks like a foreign language into which we translate our MathematiCS. I want Lean to be our native language for all MathematiCS.

I'm afraid most people studying pure mathematics still don't want to learn computer languages. A mathematics professor I met last week had no interest in learning Lean; he only wanted to use a powerful AI that helps mathematicians find new valuable results.

[Martin Dvořák]

True. I should have written "in distant future".

[Bulhwi Cha]

Maybe we should write more introductory textbooks teaching logic, mathematics, and computer science in Lean. Some students might want to learn Lean and these subjects simultaneously.

I'm no longer a student because I left my university earlier than planned. But I'll teach myself formal sciences with Lean and Mathlib. Lean is my second computer language for learning mathematics. (The first one is Metamath.)

[Trebor Huang]

It would actually be very alarming if natural language for mathematics is completely supplanted by a mechanically checked language. No matter how flexible Lean is it would not be as flexible as natural languages. And in the distant future mathematics can and will undergo revolutions that makes a large part of what is known now obsolete. A mechanically checked language would be a hinderance, just like how old notation is a hinderance, but much more severe. That's my opinion anyway, and Lean might have something by then to counteract this, who knows

[Bulhwi Cha]

Trebor Huang said:

No matter how flexible Lean is it would not be as flexible as natural languages.

If Lean were as flexible as natural languages, I wouldn't use it because I want moderate restrictions on natural languages. Lean doesn't need the full power of natural languages to represent mathematical knowledge in a human-readable way. Some controlled natural languages (CNLs) as export formats of Lean source files would suffice.

[Trebor Huang]

Bulhwi Cha said:

If Lean were as flexible as natural languages, I wouldn't use it because I want moderate restrictions on natural languages.

Yes, that's an argument that this will never happen, which is my point: Lean will never be that way.

[Trebor Huang]

I'm not saying that Lean doesn't have the ability to be like that if the designers wanted it to. I'm saying that Lean is deliberately not that way.

[Bulhwi Cha]

Trebor Huang said:

Yes, that's an argument that this will never happen, which is my point: Lean will never be that way.

Then it wouldn't sound very alarming if Lean and its associated CNLs substantially supplanted natural languages for mathematics.

[Trebor Huang]

I think the better part of Lean to be popularized/standardized is some particular viewpoints, like stressing the difference of (say) a ring and itself considered as its own ideal, or using filters to organize limits etc. The HoTT book is working in this direction: It is explicitly not formal, but nevertheless contains many viewpoints generated from the formalization process.

[Trebor Huang]

Bringing this back to the thread topic, this would enable us to refer to these ideas without having to convince a colleague that this is not some "weird foundational quirk"

[Trebor Huang]

Thus will make for better publishability, because the community acceptance is higher

[Arthur Paulino]

Talking about natural language and formalized mathematics, my main barrier when I was learning how to use tactics was translating small steps that we usually do in informal maths into tactics. So I just had an idea.

Imagine a tactic natlang that prompts a text box widget in the infoview and accepts instructions written informally. Then it processes it and tries to output the corresponding tactics that does what the user said. The output would be in form of a Try this: ...

[Eric Wieser]

Why bother with a tactic you have to type? the text box could just always be there.

[Arthur Paulino]

That's even better, yes, but that would have to be implemented in core I believe?

[Arthur Paulino]

Either way, the core of the idea is having a translation from small steps written in natural language into a sequence of tactics

[Junyan Xu]

LeanAide doesn't need a text box ... In general, OpenAI's Codex expects that you write comments and it will fill in the code.

[Siddhartha Gadgil]

Junyan Xu said:

LeanAide doesn't need a text box ... In general, OpenAI's Codex expects that you write comments and it will fill in the code.

Thanks for mentioning this. Indeed in general a comment can be picked up by a code action. Since this is not fast enough at present it will need to be lazy and explicitly invoked, but in the longer run running fast/async may be possible.

[Alex Kontorovich]

Just my two cents, but there is an already existing long-established tradition and protocol by which pure mathematicians give each other "credit" for work done (which turns into academic jobs, tenure, etc etc), namely publications in respected math journals (not CS, not conference proceedings, etc). I don't see anything in the short- to medium-turn in math culture that will change that. What makes a journal "respected"? Largely, the editorial board, and the decisions said board makes to publish what it sees are the highest quality submissions that it receives (or solicits). So if people who spend a lot of time formalizing mathematics want to get such credit, I think it's essential that there be a pure math journal devoted to reporting (in ways already described by others) on major advances in this field. Moreover, I think it's clear that the formalization community benefits significantly when more pure-trained mathematicians are drawn into it; rewards of the type that lead to aforementioned "credit" can accelerate this process. I've been working with an organization to create an infrastructure to allow very high quality Diamond open access journals to be formed for very low cost, and low time commitment for the editors (which is how you draw high-quality people, who have severe demands on their time). I'll leave it at that...

[Martin Dvořák]

Trebor Huang said:

It would actually be very alarming if natural language for mathematics is completely supplanted by a mechanically checked language. No matter how flexible Lean is it would not be as flexible as natural languages. And in the distant future mathematics can and will undergo revolutions that makes a large part of what is known now obsolete. A mechanically checked language would be a hinderance, just like how old notation is a hinderance, but much more severe. That's my opinion anyway, and Lean might have something by then to counteract this, who knows

I cannot stop thinking about this issue. Let me outline my personal thoughts...

On the one hand, I am concerned that if I keep using mathematical notation on paper then I will never become fluent in Lean because Lean will stay as a "foreign language" to me, which I "translate" MathematiCS into. Writing stuff in Lean notation on paper does not necessarily mean that I must write everything formally; I'd rather write stuff in a Lean-based pseudocode (so that I don't have to be explicit about all details but I will keep training my brain to work with the Lean notation).

On the other hand, I am worried that using Lean notation on paper would be a hinderance, no matter how much I get used to it. Lean is inherently designed to be "one dimensional" -- everything is written as a sequence of symbols. There is possibly a great value in mathematical notation being "two dimensional" -- you can write stuff above and below other symbols (not just lower and upper indices but terms of any length). Maybe Lean notation cannot be tweaked on paper in such a way that I will get the benefits of not having to write everything into a line.

[Yaël Dillies]

That dimensionality issue will likely be fixed by widgets.

[Martin Dvořák]

PS: I admit that, when I write my thoughts down, I realize I sound like a moron -- basically I am saying something like "give me one language that I can use for the rest of my life so that I will never have to learn anything new".

[Alex Kontorovich]

Since some of you asked about this, you might have a look here... https://jexpmath.org/index.php/jem/about/editorialTeam

[Siddhartha Gadgil]

Alex Kontorovich said:

Since some of you asked about this, you might have a look here... https://jexpmath.org/index.php/jem/about/editorialTeam

Does the scope of the journal include formalization? It is not clear from the description on the website.

[Junyan Xu]

Editor-in-Chief Jacob Tsimerman notably signed both https://futureoflife.org/open-letter/pause-giant-ai-experiments/ and https://www.safe.ai/statement-on-ai-risk

[Alex Kontorovich]

Siddhartha Gadgil said:

Alex Kontorovich said:

Since some of you asked about this, you might have a look here... https://jexpmath.org/index.php/jem/about/editorialTeam

Does the scope of the journal include formalization? It is not clear from the description on the website.

Not necessarily. At Exp Math (the Taylor Francis journal), we ran one special issue on it, but I don't know if the new journal will be interested. It's really a pure math journal reporting on strange, suggestive patterns discovered in one field that likely require eyes from another field to make significant progress....