Anders Lundstedt: Formalizing ellipsis usage
Time: Wed 2025-03-12 10.00 - 12.00
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Participating: Anders Lundstedt
Abstract
Ellipsis usage is useful in (non-formalized) mathematical practice. For a very simple example, consider an ellipsis definition of a partial sums of the natural numbers function: \(\Sigma(n) ≔ 0 + 1 + 2 + \dotsb + n\). Some, for example Russell O'Connor (2011),¹ has pointed out that such usage may make formalization more difficult. I discuss to what extent such usage is a problem for formalization. I present a solution that should allow for more or less straightforward formalization in dependently typed type theories of at least some uses of ellipsis. While I have not actually done the formalizations, I applied similar ideas in my (2015) MSc thesis to formalize ellipsis usage.
¹ O'Connor credits the Reddit user scrhopp for the observation.
Lundstedt, Anders (2015): Realizability in Coq. MSc thesis in mathematics; KTH Royal Institute of Technology; Stockholm. https://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-174109
O'Connor, Russell (2011): Why is it so difficult to write complete (computer verifiable) proofs? MathOverflow answer. https://mathoverflow.net/q/51782