I'm thinking of a news RSS feed/newsletter filled with GRE-level vocabs. The idea is to encounter to GRE vocabs more frequently, hence memorize the vocabs faster.

the infographic in the deepmind blog showed the team built a formalizer network. i wonder how you guys build it. last time i tried chatgpt to translate a math problem into lean it sucks

LeanDojo (at least as original published) did not use automatically formalized data, but extracted examples from Mathlib, which is already written in Lean.