AI use in my research
I use AI tools in parts of my mathematical workflow, including mathematical exploration, formalization, literature organization, and the preparation and revision of mathematical text. This page gives a public account of the token usage recorded by those tools.
An AI agent extracts these figures automatically from retained local tool logs; I do not enter or check the individual token counts manually.
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
For usage that falls under a specific project or recurring activity, the table gives a more detailed breakdown. These figures should be broadly representative, but may slightly undercount actual project-level usage where an individual AI interaction could not be matched reliably to a particular project. I expect to expand this list over time.
| Project or activity | Fresh input | Cached input | Generated output |
|---|---|---|---|
| Agda formalization work | 232M | 4.91B | 27.5M |
| Stable Homotopy Theory and Higher Algebra | 105M | 2.13B | 13M |
| Synthetic category theory | 30.7M | 782M | 3.64M |
| Gestalten | 28.2M | 481M | 3.54M |
| Hammock localization | 11.5M | 234M | 2.47M |
| Lectures on Higher Topos Theory1 | ≥ 6.17M | ≥ 175M | ≥ 1.19M |
| 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 | 584K | 22.4M | 124K |
| Relative Rezk nerve | 1.18M | 7.18M | 115K |
| Twisted ambidexterity | 274K | 1.28M | 16.1K |
1 Some Claude Code sessions for this project were lost due to Claude Code's local-transcript retention policy. The figures in this row are therefore lower bounds.
These figures are a dated snapshot, not a live counter. Exact machine-readable figures are available in JSON format.
How to read these figures
Fresh input consists of input processed without a cache read. Cached input is repeated context reported as served through provider caching. Generated output includes separately reported reasoning tokens. These classes are shown separately because they should not be assumed to have the same computational cost.
These figures record the scale and composition of my AI use. They are token counts reported by the tools, not measurements of energy use or emissions. I do not convert them to carbon or water figures because the necessary model-, hardware-, and data-centre-specific information is not available to me.
Measurement method
The figures are derived from explicit token-usage records in retained local Codex and Claude Code transcripts. The extraction itself is performed automatically by a deterministic Python script, which reads these records, normalizes the different counter formats used by the two tools, and assigns each transcript to a project from its working directory or from a reviewed manual classification. An AI agent invokes the script when the figures are refreshed, but does not read or transcribe the individual records. The script does not reconstruct token counts from prompts or estimate them from text length.
Codex generally records cumulative counters, whereas Claude Code records usage for individual assistant responses. To avoid double counting, the collector retains only the final snapshot of each Codex counter epoch, counts repeated Claude response identifiers once, uses only the latest observation of a resumed session, and ignores copied subagent transcripts.
The record does not cover deleted transcripts or AI use in unsupported clients. Project attribution is made at the level of a complete session, since the logs do not provide a trustworthy per-token division when one session concerns several projects.