Lean 4 formalization of infinitary logic and model theory: Scott/Karp, Morley–Hanf, Craig interpolation, López–Escobar, etc.
proof-assistant formalization mathematical-logic model-theory mathlib lean4 descriptive-set-theory infinitary-logic
-
Updated
Aug 1, 2026 - Lean