Theorem Proving in Lean

Hieronymi, Philipp ; Karve, Vaibhav; Blanchard, Eion; Harman, Scott; Ravi, Nikil; Zhao, Fenglong; Thompson, Kyle; Xu, Tianfan; Schargorodsky, Joel; Wulffraat, Noble

Permalink

https://hdl.handle.net/2142/115963 Copy

Description

Title

Theorem Proving in Lean

Author(s)

• Hieronymi, Philipp
• Karve, Vaibhav
• Blanchard, Eion
• Harman, Scott
• Ravi, Nikil
• Zhao, Fenglong
• Thompson, Kyle
• Xu, Tianfan
• Schargorodsky, Joel
• Wulffraat, Noble

Issue Date

2020-12-21

Keyword(s)

• mathematics
• model theory
• automated theorem proving

Abstract

Theorem proving uses computers to prove or verify mathematical statements. In this project, we formalize several ideas in model theory using a theorem prover called lean. We have successfully formalized notions such as languages, structures, terms, formulas, sentences, and models, and have made some progress towards formalizing o-minimality. The code can be found athttps://github.com/vaibhavkarve/igl2020.

Type of Resource

text

Language

en

Owning Collections