This site collects notes and progress reports for the Automated Theory Construction project.

The repository explores how LLM-based agents and Lean can be combined to:

  1. formalize candidate statements,
  2. verify proofs or counterexamples in Lean,
  3. and propose useful next problems that expand a theory rather than only solving isolated goals.

Current code lives in the main repository: tukamilano/Automated_Theory_Construction

If you work on related topics in logic, theorem proving, or formalized mathematics, feedback is welcome.