Model Theory in Lean

Table of Contents

In this project, we formalize first-order logic, languages, structures and models in Lean. The end goal is to formalize o-minimality. This project is being run (Fall 2020 & Spring 2021) as part of the Illinois Geometry Lab at UIUC.

GitHub code repository

1 Collaborators

  • Tyler Behme
  • Eion Blanchard
  • Scott Harman
  • Philipp Hieronymi
  • Nikil Ravi
  • Joel Schargorodsky
  • Kay Thompson
  • Noble Wulffraat
  • Tianfan Xu
  • Andrew Yin
  • Fenglong Zhao

2 Talk given at the LeanTogether 2021 conference

Author: Vaibhav Karve

Created: 2021-04-08 Thu 10:50