Public Library of Science staff union statement

This message, which arrived in my Inbox today, should be of interest to all colleagues who are concerned about the future of scientific publishing, including but not limited to those who signed the Cost of Knowledge statement over 10 years ago.

More information can be found at the PLOS Union website.

---

We’re reaching out to you today from PLOS, a nonprofit, Open Access publisher with journals covering all areas of science and medicine, to share some very exciting news: a supermajority of PLOS’s editorial and production staff have decided to form a union. We are wholly dedicated to our work, and committed to PLOS’s mission and the advancement of Open Access science. Unionizing will ensure that we receive the resources and support we need to maintain the standard of excellence upon which PLOS built its reputation.

After months of planning, organizing and collaboration, the time has come; on 12 May 2023, the PLOS Union formally submitted a request to have PLOS management recognize our union, which comprises the overwhelming majority of PLOS’s editorial and production employees. 

We are asking for solidarity from respected members of the academic community during this stage, which is why we are reaching out to you! Having the backing of the scientific community will demonstrate to PLOS leadership the importance and significance of our organizing efforts. Here are some ways you can help our union:

– Please find links to our Twitter and Instagram pages here: Twitter, Instagram. Please use your social media platforms to reshare, comment, like and distribute the news of our campaign as widely as possible.

– Please also follow this link here to fill out a webform in support of our union. Once submitted, it will send a message directly to PLOS leadership and let them know you are in solidarity with our organizing efforts.

Please spread the word however else you may be able to on the day of the launch. Please also don’t hesitate to reach out if you have any questions about our campaign and what you can do to get involved. Your backing plays a meaningful role as PLOS’ workers fight to achieve the working conditions they deserve.

In solidarity,

The PLOS Union

https://plosunion.org/

Advertisement

News Flash: Is this the Singularity?

A new post on Silicon Reckoner asks whether the Singularity may have come and gone while attention was focused elsewhere.

Manjul Bhargava’s lecture at the Mazur conference is finally online

In 2018 Harvard held a week-long celebration for Barry Mazur’s 80th birthday. In keeping with Mazur’s wide-ranging interests, and with the title — Mathematics Is a Long Conversation — the middle day was devoted to panel discussions on topics accessible to the general public. That day’s program concluded with a public lecture by Manjul Bhargava entitled Poetry, Drumming, and Mathematics. Bhargava explained how mathematical principles were discovered in India, as far back as the 3rd century B.C., in connection with poetic meter and rhythms in drumming.

To say more would be to deprive the viewer of the pleasure of discovering these connections at the pace at which Bhargava chose to reveal them. This pleasure can now freely be enjoyed at the IHES YouTube site, which has just uploaded Oliver Ralfe’s video of Bhargava’s talk.

Replies to my fan mail

A place for reactions to and questions about siliconreckoner.substack.com.

…beyond my interest in how current trends in mechanization of mathematics force me to sharpen my own understanding of what makes mathematics valuable as a human practice (as in this close reading of a magnificent lecture by Dick Gross), I am deeply interested in mechanization of mathematics, of which formalization is a small part, as a social phenomenon: how it establishes a shared vocabulary, an ideology, a system of values, a community; how it overlaps with and is influenced by broader economic and industrial trends; what it does or does not share with contemporary political movements; and much more. In this respect the leanprover-community Zulip Chat Archive is a veritable socio-historical goldmine. And with that in mind I encourage you to direct your comments to this page.

Is the AMR really the anti-woke fortress in mathematics?

And what does this have to do with mechanization?

…nothing evokes as much hostility among intellectuals as the suggestion that social forces influence or even dictate either the scientific method or the facts and theories of science.

(Richard Levins and Richard Lewontin, The Dialectical Biologist)

Last October 24 I unexpectedly received the following message from an extremely eminent colleague who had been invited to join the brand new Association for Mathematical Research, an organization of whose existence I had been unaware until then:

the thing that puzzles me is why do we need a new Society devoted to research? Especially since its mission statement is just: ‘research.’  I’m already a member  of a number of them.  Is there a subtext I’m not getting here? 

Continued at Silicon Reckoner. Comments welcome here, as always.

Luddites are misunderstood

Any change in technology leads almost inevitably to an improvement in the welfare of some and a deterioration in that of others. To be sure, it is possible to think of changes in production technology that are Pareto superior, but in practice such occurrences are extremely rare. Unless all individuals accept the “verdict” of the market outcome, the decision whether to adopt an innovation is likely to be resisted by losers through non-market mechanism and political activism.

(Joel Mokyr, The Political Economy of Technological Change: Resistance and Innovation in Economic History.) 

…Two weeks ago I quoted Jasmin Blanchette, a Dutch computer scientist who complained about “proofs [that] look more like LSD trips than coherent mathematical arguments.” I thank Alex Best for informing me that the expression goes back to the very interesting Teaching Statement that Scott Aaronson posted in 2007. Blanchette sees formalization as a remedy, but it occurs to me that the comparison cuts both ways. Most people who write about that sort of thing claim that enlightenment is what is sought by those who take steps to achieve altered states — through wine, poetry, virtue, meditation, or a drug like LSD. Enlightenment is also what I am seeking in a mathematical proof, and I’m sure most of my colleagues feel the same way. Nick Katz likens a routine sort of mathematical enlightenment to Molière’s M. Jourdain, realizing that he is speaking prose. Most precious are the rare proofs that induce a sense of transcendent bliss, bringing tears to one’s eyes. No such weeping with joy, either by programmer or by machine, has yet been recorded in the annals of formalization.

In connection with today’s entry, however, I am thinking of a different form of enlightenment. Imagine that in your condition of heightened consciousness you find yourself speaking a throwaway word mechanically — like “luddite.” Suddenly you tell yourself that what you hear is not only nor even primarily your own voice, but the entire history of semi-conscious associations that planted that word in your manifest vocabulary. While this is obvious in retrospect, it is only your altered state that impresses upon you the realization, the intimate feeling, that it is the word, with its accretion of dead slogans and long unexamined thoughts, that is speaking through you, and not the other way around. In this situation — here I have to tread carefully, to protect my professional reputation — enlightenment can be experienced as a form of liberation.

The essay continues at siliconreckoner.substack.com.

The Central Dogma of Mathematical Formalism

For mathematical formalists, a proof is a sequence of valid formulas in a symbolic language, each obtained from the previous one (more likely the conjunction of several) by a legal transformation (rule of deduction), or the statement of an axiom.

A theorem is then any valid formula that appears as the final statement in a sequence.

Here is a recent militant but unsubstantiated attempt to ventriloquize mathematics in support of this Central Dogma:

an informal mathematical statement is a theorem if and only if its formal counterpart has a formal derivation. Whether or not a mathematician reading a proof would characterize the state of affairs in these terms, a judgement as to correctness is tantamount to a judgment as to the existence of a formal derivation, and whatever psychological processes the mathematician brings to bear, they are reliable insofar as they track the correspondence.                                                    (Jeremy Avigad, 2020)

Avigad, as you see, actually writes “if and only if.” …

The distinction between “if” and “only if” is in any case lost on the public when the Dogmatic position is supported, as Avigad’s is, by a new $20,000,000 institute as well as the backing of a 33-year-old cryptocurrency billionaire who is rumored to be willing to donate ten times as much over the coming years.…

The complete essay can be read on the Silicon Reckoner Substack newsletter. Comments welcome here.

What is human-level mathematical reasoning?

William Thurston speaking at Harvard in 2007.

Mathematics is unpredictable. That’s what makes it exciting. New things happen. William Thurston, May 14, 2007

It’s a gloomy, rainy, almost wintry day in Paris, which I don’t always love when it drizzles, and I’m starting to write the next entry in this newsletter, trying to figure out what, if anything, Christian Szegedy had in mind when he predicted, as I reported a few weeks ago, that “Autoformalization could enable the development of a human level mathematical reasoning engine in the next decade.” Is there exactly one “human level”? The expression is common among the knights of the artificial intelligence community, whose grail is something called “human level general AI.”

Part 1 of the text continues.

Can mathematics be done by machine? I.

Notes of a Columbia course with Gayatri Chakravorty Spivak and special guest Kevin Buzzard

Summary

Proof, in the form of step by step deduction, following the rules of logical reasoning, is the ultimate test of validity in mathematics. Some proofs, however, are so long or complex, or both, that they cannot be checked for errors by human experts.  In response, a small but growing community of mathematicians, collaborating with computer scientists, have designed systems that allow proofs to be verified by machine. The success in certifying proofs of some prestigious theorems has led some mathematicians to propose a complete rethinking of the profession, requiring future proofs to be written in computer readable code. A few mathematicians have gone so far as to predict that artificial intelligence will replace humans in mathematical research, as in so many other activities.

---

Mechanization of what mathematics?

One’s position on the possible future mechanization of proof is a function of one’s view of mathematics itself.

Is it a means to an end that can be achieved as well, or better, by a competent machine as by a human being? If so, what is that end, and why are machines seen as more reliable than humans?

Or is mathematics rather an end in itself, a human practice that is pursued for its intrinsic value? If so, what could that value be, and can it ever be shared with machines?

The remainder of the article is at Silicon Reckoner.

Intelligent Computer Mathematics vs. Intelligent Mathematics

Part I: A review of Christian Szegedy’s “Promising Path”

“Grothendieck’s way of writing is based on an atypical conception of mathematics, described and theorized in texts [that] vigorously bear witness to the unavoidable poetic aspect that motivates scientific work and the surplus of meaning that formalization believes should be eliminated, although this surplus is precisely where the essence of mathematical thought lies.”                 (F. Patras, La pensée mathématique contemporaine, Introduction)1

This week and the next I compare two perspectives on the “the surplus of meaning” and “the essence of mathematical thought,” both implicit in texts about mathematics:  the first by a prominent exponent and prophet of “intelligent computer mathematics,” the second by a prominent number theorist.  It would be too easy to say that the first text takes the position that there is no surplus and that the “essence of mathematical thought” resides in formalization and nothing more, while the second text exemplifies the surplus of meaning as well as what one reviewer of Karen Olsson’s book The Weil Conjectures (to which we return in Part II) called “the poetry and precision of a theorem.”  What, after all, is an “essence”?  Philosophers have worried about this for millenia, with some interruption, asking for example in what sense the essence of Socrates resembles that of being an even prime number, and have failed to arrive at consensus on the essence of “essence.”  The whole confusing history is recorded in the Stanford Encyclopedia of Philosophy’s entry on “Essential vs Accidental Properties” (which, troublingly, includes no references in French).…

The complete text has been published on my Silicon Reckoner Substack newsletter.