Synthetic formulations

formal_conjectures has a critically important role in math - providing a global repository of formalizations for AI-assisted team generated math.

the human oriented mathlib approach may misunderstand the problem. lean machinery has proven difficult and awkward to manually re-use. getting results merged into mathlib itself is problematic as well.

better perhaps would be to have formalized template examples of different known theorems and machinery which AI can adapt for specific use cases. this blending and adaption is something AI can do very well.

to that end, i suggest that formal_conjectures should embark on a mass synthetic data generation effort.

the way to do this could be to start proving higher theorems using frontier LLMs using informal reasoning. Then ask the AI systems what's involved in formalizing and what machinery is not readily available. Each of those points becomes a target to formalize and add to this repo. this ask just needs to be for motivation, it doesn't even need to be a complete proving of the original higher theorems which can be unsolved open problems themselves.

as the resulting machinery will be mostly known results, most of it likely can be quickly autoformalized and the repo would expand without restraint to encompass large swaths of formalized known math.

in turn, systems which need to formalize harder problems can use these pre-computed results as templates to follow for their own results rather than having to constantly reformalize basic but missing machinery.

ofc, it's not all that magically simply and some serious thought needs to go into the best way to organize the effort so that there is unnecessary duplication and maximum effective RAG reuse is possible. For this, it's possible we can have a larger raw collection which we can experiment with on different methods of auto-curation into better organized mini synthetic repos until the process is strong. this will also help inform how end-use RAG and adaption (the biggest ? in all of this) might work itself. occasional reworking to integrate newer version of mathlib may be appropriate if proven productive.

The reason this is all imminently important is that right now there is a massive bottleneck in team generated, AI assisted math which requires formalized results. With solo work, informal reasoning works fairly well, but as you scale up to large groups and partition the work, formalization becomes required. Until we get the repo above we can't start engaging in this productively. It also seems to be a waste of compute for everyone to be reformalizing everything from scratch.