Weak and strong normalization in pure type systems

Fork of openai/math containing only the Lean proof of this paper, with nanoda enabled in the comparator challenge (see comparator-run.log).

Author: OpenAI

Date: September 25, 2026

Citation

@misc{OAI:Weak-and-strong-normalization-in-pure-type-systems-September-25-2026,
  author = {{OpenAI}},
  title = {{Weak and strong normalization in pure type systems}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf}{OAI:Weak-and-strong-normalization-in-pure-type-systems-September-25-2026}},
  year = {2026}
}