Theorem prover Arend.

arXiv:2610.27264v2 Announce Type: replace-cross Abstract: This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the framework of univalent