Ability to attach a theorem prover to be able to work on more formal math&logic parts

[erkinalp]

When coupled with a theorem prover, the capacity may increase significantly.

[BradKML]

Which software libraries do you have in mind?

[erkinalp]

https://github.com/leanprover/lean4
https://github.com/higherorderco/kind

[BradKML]

Does any of these tools ring a bell for provers? How do they differ from one another as non-agent tools?

• https://github.com/lean-dojo/LeanCopilot + https://github.com/lean-dojo/ReProver
• https://github.com/wellecks/llmstep
• https://github.com/jesse-michael-han/lean-gptf + https://github.com/jesse-michael-han/lean-step-public
• https://github.com/cmu-l3/llmlean