Proven correct: business logic with Lean and AI

Lean is a programming language for writing mathematical proofs, so instead of testing your software and hoping, you prove it correct. Matthias has been pairing Lean with AI to try exactly that on real business problems: building proofs for accountants, construction projects, and other domains where the books have to balance and the schedule has to hold. Come see what a theorem prover actually does and how AI changes the work of writing proofs, and leave motivated to write robust software that is mathematically proven to be correct.