AI use in my research
I use AI tools for mathematical exploration, formalization, literature organization, and the preparation and revision of mathematical text. This page records how many tokens those tools report that I have used.
An AI agent extracts these figures automatically from retained local logs. I do not enter or check each token count by hand.
The totals below cover all recorded usage classified as related to my mathematical work.
This AI disclosure page should be treated as experimental. At present, it is unclear to me what the standards around disclosure of AI usage should be, and whether the presentation here is suitable. Given the wide range of opinions about AI usage in mathematics, I think that clear transparency about token usage is nevertheless helpful.
Selected projects and activities
When usage can be assigned to a specific project or recurring activity, the table gives a more detailed breakdown. These figures should be broadly representative, but may be slightly too low because some individual interactions could not be matched reliably to a project. I expect to add further projects over time.
| Project or activity | Fresh input | Cached input | Generated output |
|---|---|---|---|
| Agda formalization work | 233M | 4.91B | 27.5M |
| Stable Homotopy Theory and Higher Algebra | 117M | 2.35B | 13.9M |
| Lectures on Higher Topos Theory | 32.9M | 1.1B | 4.4M |
| Synthetic category theory | 35.6M | 894M | 4.33M |
| Gestalten | 28.2M | 481M | 3.54M |
| Hammock localization | 11.5M | 234M | 2.47M |
| Parametrized spans | 8.27M | 198M | 781K |
| Universality of Span 2-categories | 4.79M | 65.5M | 513K |
| Global spaces and the homotopy theory of stacks | 1.77M | 45.1M | 185K |
| Webpage maintenance | 1.25M | 36.7M | 167K |
| Relative Rezk nerve | 1.18M | 7.18M | 115K |
| Twisted ambidexterity | 274K | 1.28M | 16.1K |
These figures were last updated on the date shown above and do not update automatically. The exact figures are also available in JSON format.
How to read these figures
Fresh input is input processed without using a cache. Cached input is context that the provider reports as having been read from a cache. Generated output includes reasoning tokens when these are reported separately. I list these three categories separately because they may not require the same amount of computation.
These figures show how many tokens I have used and of which kind. They come from counts reported by the tools, not from measurements of energy use or emissions. I do not translate them into carbon or water figures because I do not have the necessary information about the models, hardware, and data centres involved.
Measurement method
The figures come from token counts stored in local Codex and Claude Code transcripts. When this page is updated, an AI agent starts a Python script that reads the counts automatically. The script accounts for the different ways in which Codex and Claude Code store them, and assigns each transcript to a project based on its working directory or an explicit classification recorded in the ledger. The agent does not enter the individual counts by hand. The script also does not try to infer token counts from the prompts or from the length of the text.
Codex usually keeps a running total, while Claude Code records usage separately for each assistant response. For Codex, the script uses only the last total before the count starts again. For Claude Code, it counts each response once and uses only the most recent copy of a resumed session. It also ignores duplicate transcripts made for subagents.
The figures do not include deleted transcripts or AI use in applications from which the script cannot obtain token records. Each session is assigned to one project as a whole. If a session concerns several projects, the logs do not provide a reliable way of dividing its tokens between them.