For context: Consider me Gas Town level 6 but I am hesitant about the CLI. - —So I am currently working on a large math proof. I have almost 600 compiled lean modules and an extensive sprawling math project that includes API’s and HPC optimizations so I can run complicated code on an ‘underpowered’ system (dont knock my PC 
- Yes its older - ). Of course the solution requires ‘exactness’, and the system has been attempting to round, optimize, and ‘limit/bound’ its way out of it. But I have it pretty well nailed down. – I am down to the final lemmas and connections. It does produce the required calculations and can present the LEAN path. – however – once I start drafting the lean there is drift. It will miss or exclude critical lemmas, or use Mathlib arithmetic to replace my native (more robust and necessary) arithmetic. – I should be clear my proof is very ‘Set Theory’ heavy so there are sets that exist, and artimetic expressions that need to be true. But its not the same as calculating a solution for a specific problem. – My question is this :
How would you recomend working with complex solutions for new math (that doesn’t have existing mathematical language and Majority of the LLM’s thought ‘bubble’ points to impossible) while not running into a wall with Conext windows and processing limits
Here are the things I have tried to varied success:
-
Bridging any native work to mathlib. - This way if it replaces a function with the mathlib function there is a direct link that can be exploited. The problem is these connections still have to be defined. If the context window shrinks it leaves the prime relationship but not the secondary ones
-
Creating MD file logging in every prompt. In every prompt and task I am now 1- making them stepped. 2- Requiring a ‘zero step’ to outline the plan. 3- I have a specific logging directory on a shared drive. Every step an MD file is generated and uploaded to the log to retain continuity. The problem with this is it ALSO eats into the context window. Sometimes it starts taking the logging more seriously then the math. — This also introduced a bias issue due to the ‘piece by piece’ nature of LEAN and math proofs, so I also have to include a statement ensuring it does not draw conclusions from singular modules or equations as to their usefulness. Because of the step-by-step plan it was now injecting a statement into each MD file stating that this singular step was not the proof, nor did it imply a proof, etc. – So when you goto finally review the collection of modules that form the proof, even though it was accurate the LLM would read the comments and not compute the math, concluding there was no valid proof. I have this documented too lol but different issue
3)Requiring pain language reports. Having the system periodically produce a plain language, human readable, report with the project and the steps. Or having it outline the theorem and the conclusions. - This is an excelent troubleshooting tool for MANY reasons (one of which is the bias issues but that is a seperate topic). This I have moderate luck with but the problem is there are different paths to the solution. And even after it is nailed down in LEAN there are two or three ways it can be described. - So this can cause some misalignment when working with multiple instances/agents.
any advice would be appreciated.