Post by @tao@mathstodon.xyz

2026-08-06 13:47 UTC

Thanks for all the feedback! I had truncated the proposal somewhat to fit inside Mathstodon's post limits, but I realiize now I should have clarified and modified a few things. 1. "scientific lecture" should become "publicly available scientific exposition". This can include a traditional lecture, but also non-traditional formats such as expository blog posts, self-recorded video, etc.. Eventually, I hope that standard arXiv-like repositories as well as journals for expositions will appear, although the infrastructure is not there yet. (But see the new "Mathematical Discourse" journal at https://www.mathematicaldiscourse.org/ for a first step in that direction.) 2. The exposition artifact is meant to supplement the paper artifact (and the formal certificate artifact, if available), rather than replace it. So the actual "date of release" under this proposal would be max(preprint release date, exposition release date). Once autoformalization becomes routine, one can also add "formalization release date" to this max as well. More broadly, in the past we had a single artifact - the paper - that was supposed to record four separate aspects of a proof: generation, verification, exposition, and publication. In the future, we may decouple this into multiple artifacts - a generation artifact (e.g., AI chat logs), a verification artifact (e.g., Lean code), an exposition artifact (e.g., a recorded talk), and a publication artifact (the traditional paper). Priority then becomes a question of who was first to provide a complete set of artifacts. 3. "But what if AI can automatically generate good expositions also?" I would actually be happy with this outcome; cf. https://xkcd.com/810/

Replies (4)

@tao@mathstodon.xyz 2026-08-06 14:22

Here is one possible dynamic that I could envisage happening in the near future. In the future, a mathematician (or collaboration) working on a problem would typically maintain a private repository containing partial progress towards all of the goals of generation, verification, exposition, and publication: incomplete sketches, AI chats, Lean proofs with sorries, slides of a talk, etc., with timestamps recording the date each step of partial progress was achieved. The social norm would be to wait until all of these goals are achieved to at least a preprint-level of quality, then make their repository public and submit various one or more components of their work to appropriate venues (traditional journals, formalized repositories, new journals focusing on exposition, etc.). But if someone working on the problem "jumps the gun" and makes their work public before all of the desired components of generation, verification, exposition, and publication are complete, then everyone else working on the same problem will be incentivized to similarly make public their own work on the problem. Discussions can then take place between these parties as to whether to combine efforts, or aim instead for simultaneous publication; but the social norm would be to not automatically reward the first to disclose one component of a solution with the credit of priority. (Some collaborations may be "Polymath style" and open from the outset. The social norm would then be for others interested in the problem to work with that collaboration, rather than directly compete with it.)

Open ##5165711
@human_in_exile@mathstodon.xyz 2026-08-06 13:49

@tao@mathstodon.xyz But if its going to be made in NL for humans to understand anyway, like a journal, would people feel a need to formalise? At no stage really did someone say “my biggest issue with reading math journals is a computer didn’t mechanistically verify it in a language I do not understand” (or not many did if so, at least). There is never even a burden of understanding on the journal editors , they must usually assume you are wrong , and be convinced otherwise , in NL. As soon as they are confused they just stop reading and send it back, and if it was too "AI" you’d probably get black listed regardless of an attached theorem prover repo.

Open ##5165741
@torgeirlysen@mathstodon.xyz 2026-08-06 13:56

@tao@mathstodon.xyz I think there is something inherently social about exposition. Grant Sanderson recently said something about this in his podcast appearance with Dwarkesh Patel. That we will probably want human curators and teachers no matter how advanced the AI gets.

Open ##5165743
@utkarshare@mstdn.social 2026-08-06 14:57

@tao@mathstodon.xyz will human mathematical problem solving become an extinct skill in the very near future (next decade or two)?

Open ##5165746