Development

Math, Inc. autoformalizes a web of Tao's estimates

development2026-01-08

Claim

Math, Inc. partnered with Terry Tao to autoformalize an entire web of estimates in analytic number theory.

Reporting date: 2026-01-08 (not necessarily the event date)

Sources

Attribution and reporting linked by this record; links do not imply independent verification.

Welcome to January 8, 2026 (theinnermostloop.substack.com)

Knowledge graphopen in browser →

Reported in

Welcome to January 8, 2026

Actor

Evidence for

Supersedes

An Erdős problem is solved before any human solves it

Referenced by

Cite or correct this record

Citation formatCitation text

Math, Inc. autoformalizes a web of Tao's estimates
Innermost Loop KB — secondary record
Reporting date: 2026-01-08
KB permalink: https://nicholsn.github.io/innermost-loop-kb/developments/2026-01-08-math-inc-autoformalizes-tao
Claim: Math, Inc. partnered with Terry Tao to autoformalize an entire web of estimates in analytic number theory.
Attributed sources:
- Welcome to January 8, 2026 — https://theinnermostloop.substack.com/p/welcome-to-january-8-2026
This citation does not imply independent verification of linked-source claims.

Suggest a correction — opens a GitHub draft for you to review and submit.