Tianyi Peng

Anthropic researcher and assistant professor at Columbia, whose group builds tools for AI formalization. He set the FLT effort going to test whether Claude could make progress on it, and supplied the only mathematical steering the run received — instructions at the level of "Jacobian as a scheme sounds high priority" flt-formalization-anthropic. He is also a co-author of prove2me, the platform the successful run depended on.

Anthropic's own footnote gives the motive: as an undergraduate Peng lost a Nature publication because, asked whether a long proof of his was correct, he answered honestly that he was 99% sure and could not be certain. The person who built the verification tooling had been on the wrong end of the verification problem.

Related

flt-formalization-anthropic · prove2me · autoformalization · anthropic