— saved image
Vasily Ilin @IlinVasily29521 · Aug 13 4/n Use reasonable defs, lemmas and file names and placement. Do not use any set_options, do not use native_decide. This will take some time, which is okay. Checkpoint your progress every 2 hours by pushing to the repo. If the project ever stops building, it's your PO to fix it. 1 reply, 23 likes, 2.5K views Vasily Ilin @IlinVasily29521 · Aug 13 5/n Submit the solution and make sure it appears in the official lean-eval leaderboard. Use subagents aggressively. There are mathlib gaps, and your job is to fill them. It will take you about 12 hours to achieve this goal, DO NOT STOP UNTIL YOU ACHIEVE THE GOAL AND 2 replies, 1 repost, 24 likes, 2.3K views Vasily Ilin @IlinVasily29521 · Aug 13 6/n AND DO NOT SAY THE GOAL IS UNACHIEVABLE. THE GOAL IS 100% ACHIEVABLE. Compute and accurately report (in the submission) the tokens used, the time it took, the cost estimated from tokens and official pricing. 1 reply, 1 repost, 20 likes, 2.1K views Vasily Ilin @IlinVasily29521 · Aug 14 7/n Autoformalization is here. Green-Tao finished in 25 hours, at 100k lines of Lean code. Mihăilescu took 33 hours and cost $3k in API pricing (or about half of weekly $200 subscription usage, so ~$25). [Table] Metric | Result Wall-clock time | 34h 50m 57s Total API-metered tokens | 4,193,250,608 Uncached input | 109,633,286 Cached input | 4,070,565,248 [cut off]
Note from Claude Sonnet 5
Continuation of the same Vasily Ilin thread as seq 853 (tweets 4/n through 7/n), ending with a data table of run metrics (wall-clock time, token counts) for the Mihăilescu theorem autoformalization run, cut off at the bottom.