LeanDetective - Can AI solve murder mysteries?

I will talk about LeanDetective, an open-source Lean4 library I created which acts as a Domain-specific language to model detective mysteries such as Drishyam or Knives Out.

Lean4 uses Dependent Type Theory, where propositions become types, and programs become proofs. This makes it possible to prove properties of programs within the same environment.

I will introduce basic techniques like inductive types, modeling spatio-temporal histories, pluggable physics models and using them to establish theorems like "Prime suspect is whoever had the motive, means and opportunity".

This also gives a glimpse on how math and programming languages will increasingly open more domains and roles to AI agents, such as crime detectives, lawyers and perhaps judges.

• Intro to Lean4 & Dependent Types

• How to model murder mysteries in LeanDetective

• Showcase examples: Murdle, Drishyam & Knives Out