As of: 2026-10-13 07:38 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/p/2026-10-12-roberts-what-even-is-mathematical-output/

# David Roberts: 'What even is mathematical output?'

David Roberts, Blog, 2026-10-12.
Source: https://thehighergeometer.wordpress.com/2026/10/12/what-even-is-mathematical-output/

## Why it matters

A mathematician who formalises in Lean for his day job argues that mathematicians are judged by their writing, and that OpenAI's release of over 700 unrefined documents is therefore 'not just frustrating, but insulting'; he collects expert verdicts on the papers and points to junk Lean files in the repository. Posted by the author under Tao's Oct 12 reading list.

## Summary

Posted Oct 12, 2026 on the blog theHigherGeometer by David (Michael) Roberts, who linked it himself in a comment under Tao's list. Roberts says his views on AI are mixed: he uses it at work, where "we formalise things (previously in Isabelle, now in Lean)", but will not let it draft his papers. He argues that understanding in research mathematics can only be assessed through the communication of ideas, with Mochizuki's IUT papers as a case where unclear writing meant the theorem could not be held established, and that "it is mathematical writing that stands the test of time". Against that standard he sets the documents OpenAI released on Oct 6, quoting assessments by Melissa Lee (The Conversation), Asaf Karagila, Nick Kuhn (ALG-TOP mailing list), Enrico Fatighenti and Giulio Tiozzo (Proofs and Prompts). He says he has "not actually read any of the papers" himself; the two results that stood out to him were a uniform zero-free region for the Riemann zeta function and Grothendieck's homotopy hypothesis for the ∞-groupoids of Pursuing Stacks. He shows Lean files from the repository that consist only of repeated `open` statements (credited to Joseph Meyers and Sébastien Gouëzel on the Lean Zulip) and calls the missing "undergraduate-level code clean-up" striking. He mentions the parody X account @Endings500 and that unformalised papers were withdrawn from the release for errors.

## Archived text

> - "What is the actual method by which we can appreciate someone's understanding of ideas you are hearing for the first time? I argue that it is in the communication of those ideas."
> - "But, on the whole, it is mathematical writing that stands the test of time."
> - "I hope you, dear reader, can appreciate at least one aspect of why the dump of over 700 long documents of this nature is not just frustrating, but insulting."

Short quotes only; full text at the URL.

## Cited in

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/)

## People in this post

- [Terence Tao](https://postcutoff.com/person/terence-tao/), Professor of mathematics, UCLA