Two things recently have made me think again about academic publishing, at least as it is in mathematics.

There is some talk now about proof assistants such as Lean beginning to make a big impact on how we do our subject. I was talking about this with my colleague Louis Theran, who put forward the view that the bottleneck with proof assistants at present is the great labour needed to change a mathematician’s proof into the format that a proof assistant can process. Louis suggested coupling the proof assistant to an artificially intelligent chatbot, which could do this translation; you would just feed the chatbot your proof, as you might explain it to a colleague, and the rest would just happen.

This would not instantly change the proving of theorems, but it might have an effect on refereeing. There are three questions a referee might be expected to answer about a paper: Is it correct? Is it important? Is it clearly written? The first of these is by far the most important, but no journal expects referees to answer it; several journals explicitly say so, though of course with the rider that if you spot a mistake, please point it out. But if we had a proof assistant that could understand mathematician-speak, we would have a better way to certify the correctness.

This is relevant to publishing. At present, the people who judge our research and award grants rely on publication in a journal to guarantee the correctness of a paper, which it manifestly does not do, and other indicators (often deeply unsatisfactory bibliometrics) to judge its importance. I am too old to apply for grants now, and have no desire to improve my standing with the bosses, so this would suit me fine.

Which brings me to the other issue I want to address. It seems absurd to many of us that, after we do the research, write and typeset the paper, referee it, and edit the journal (all without remuneration), we have to pay thousands of dollars to get our paper into print. This used to be called “vanity publishing”; now it has been dignified with a TLA, but it is just a way of maintaining the huge profit margins that the big international companies make on academic publishing (over 30% in some cases). Apart from anything else, this money could have gone to support further research.

There has been some talk about the coming of free journals (free to both authors and readers, what we used to call “diamond open access”). Organisations like Scholastica have supported this trend. Indeed, several journals formerly published by big international publishers have been “flipped”, with the editorial board resigning *en masse* and setting up a new free journal. Usually in these cases the publisher blocks the use of the name for the new journal, so something similar has to be devised; and in many cases the publisher simply appoints a new editorial board and carries on. Now it wouldn’t take a very skilful gambler to make a good bet on which of these journals will go to the wall first.

And the point I want to make is that publishers have found a new way to lock you in, once you have submitted your paper to them. Usually the paper is rejected, but of course if you take it away this represents a loss of income to the publisher. Their first gimmick is to have a “transfer desk”, like but unlike the one in an airport. This desk offers you a selection of the same publisher’s journals, all much lower in the pecking order than the one you submitted to, and offers to transfer your paper and the referee reports to the new journal with no more effort on your part.

They have now added a new trick. I have not seen this in mathematics yet, but it certainly does exist in cognate subjects such as statistics. The conditions for submission of a paper require you to use the publisher’s class file when you prepare the paper. This involves a fair amount of work, and if after rejection you go to another publisher, this work has to be done all over again; having done it, there is even more temptation to take the suggestion of the transfer desk.

Neither of these is directly related to APCs. However, as I suggest, I believe there is a strong connection. What large company will run the risk of forgoing the vast profit to be made from publishing your paper?

But an automated proof checker could potentially answer the most important question about a paper (is it correct?) and would mean that a paper with such a certificate could be put on the arXiv and would be just as trustworthy as a paper in a refereed journal.

Bring it on!

Of course if you had to put all papers through proof checker many fields will die, some of which I will not name, but I can think of at least two fields 95% of papers are only 80% correct, but this is obscured by length.

Btw hope you are well!

Actually, one of my friends wrote the first correct proof to a 100 year old theorem, this is their most cited paper and a genius move. I know of two other theorems in my field with no completely written correct theorem.

Josh, thanks for this. When I taught maths and philosophy, I used to like shocking the students by saying, maths is anything you can get past a referee. (Those were more innocent days.)

Speaking of which, St Andrews now at last has a module on Set Theory and Logic; I have been teaching the first half of the module this semester. 45 students in a level 5000 module, so there was clearly a demand for it!

Otherwise, all well; I am getting up early this semester to help Rosemary get in to the Institute in time for her 9am lectures three days a week.

Unfortunately for the fortunes of the individual researcher, Corporate AI ChatBots are more likely to find their main use in service to IPSMOs (Intellectual Property Strip Mine Operators).

Yes, we should hope that we have friends in the AI community who are not under the corporate thumb. (See Ursula’s post below.)

For reasons I don’t understand, Ursula Martin tried to post a comment, but the system wouldn’t let her. Anyway, here it is:

Peter – there are a number of people experimenting with linking natural language (both human and auto-generated) with theorem provers. Tim Gowers thought about this quite a bit a few years ago, and one of the latest incarnations of these ideas, from a group in Cambridge, including one of his PhD students, is here https://arxiv.org/abs/2205.12615