Research keynote

on YouTube ↗42m

" summary

Formalizes the pleading stage by encoding Federal Rules into Lean, shipping a date and time library in Lean and an implemented algorithm for Rule 6 that exposes holiday, weekend and three‑day mailing edge cases; builds a typesafe US courts API to prevent non‑existent venues; attempts a docket-as-program evaluator but finds real dockets tolerate late or missing actions so deterministic dismissal rules (Rule 4 service, diversity jurisdiction) fail in practice, and pivots to a score‑delta model that gives actionable, probabilistic guidance.

AI-written summary · about

" chapters (11)

1. 0:00Keynote introduction
2. 1:52Civil procedure challenges
3. 8:12Bulls v. Russell case study
4. 11:30Federal Rule 6 in Lean
5. 17:10Research goals for legal software
6. 22:01Legal software limitations
7. 26:31Graph model for civil procedure
8. 31:07Modeling litigation challenges
9. 36:00Practical litigation lessons
10. 39:53New civil action analysis model
11. 40:35Closing remarks