Been doing something similar and I would add that playing multiple LLMs off on each other gets a far superior result. One LLM would suggest a tightening of a p

Been doing something similar and I would add that playing multiple LLMs off on each other gets a far superior result. One LLM would suggest a tightening of a particular axiom, and I would ask the rest what the consequences are: what is gained, what is lost and decide whether to use it. Often another would suggest a tweak that then goes back and a recursion.