Gödel's Poetry: AI, Lean 4 Prover
A Lean 4 multi-agent theorem proving system combining recursive decomposition, RAG-based retrieval, AST extraction, and verifier-guided proof generation.
Blog
AI at zbMATH Open – Talk by Christian Bär
Christian Bär presents how AI is used at zbMATH Open – from digitization to search and review generation.