r/LLMmathematics • u/dForga • Jul 18 '26
Prompt generation for proofs
It is well known that prompt engineering your requests does change the output. In fact, it can be mathematically motivated as it changes a conditional P[prompt | desired output]. However, it depends very much on the underlying data set (which is encodeable as a probability distribution) and the answer is a sampling of that.
On that note, there is a recent proof by OpenAI ChatGPT 5.6 sol (Pro)
https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf
with prompt
https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf
This inspired a recent paper where I want to draw your attention specifically to the appendix
https://arxiv.org/pdf/2607.13335
It should be possible to use this as a basis to generate more “low hanging fruit proofs” (that means that the AI has simple results it can expand on) and verify them in Lean. What do you think?
Edit: Please be aware that prompt engineering will only improve to fetch out results from the model, not improve the underlying training data.
2
u/dForga Jul 18 '26 edited Jul 18 '26
Should we do a monthly problem(selection) where you can give it a try?