The first version of Arend is released! Learn more at arend-lang.github.io/2019/07/17/Are…

Arend 1.1.0 is released. Arend now has proof irrelevant universe of proposition and the plugin can run the typechecker automatically in background. See arend-lang.github.io/2019/10/01/Are… for more information.

Arend 1.2.0 is released. Arend now has pattern matching on idp, which can used instead of the J operator. See arend-lang.github.io/2019/12/16/Are… for more information.

We've just finished the first part of our tutorial arend-lang.github.io/documentation/…. It covers all the basic constructions of Arend. It does not mention anything related to homotopy theory. This will be the topic of the second part.

Arend 1.3.0 is released. The main new feautre is language extensions. You can now write some Java code which will be executed during type-checking. This can be used for proof automation and to implement various syntactic operations on AST.

Valery Isaev will give a talk on Arend on Aprill 30, 12:00 EST: fmf.uni-lj.si/si/obvestila/5…. Here's a link to the Zoom conference zoom.us/j/96544395816. It

The video of the talk "Arend proof assistant" by Valery Isaev (JetBrains research) is now online. vimeo.com/413726748 Arend Language #EveryProofAssistant

The second part of our tutorial is ready! arend-lang.github.io/documentation/…

Arend 1.4.0 is released! arend-lang.github.io/2020/06/29/Are…

Arend 1.5.0 is released! arend-lang.github.io/2020/10/10/Are… This release includes improved performance and overall usability as well as some language features such as meta resolvers which can be used to implement even more flexible EDSLs.

Arend 1.6.0 is released arend-lang.github.io/2021/02/28/Are…. Arend now has efficient built-in finite types. The ring structure (and field structure for prime n) was defined on Fin n in the standard library. Also, a few new tactics were implemented in it.

Here's another talk in which we give some simple examples like a proof that the loop space of the circle is the integers youtube.com/watch?v=-lVPAw…

Arend 1.7.0 is released arend-lang.github.io/2021/09/06/Are…. This release includes built-in arrays, pattern matching in lambdas, multiple level parameters in definitions, and several IDE features such as auto-import of missing instances and "extract function" intention

There is a new tutorial on interactive theorem proving with IntelliJ Arend. Check it out to learn about the features of IntelliJ Arend that speed-up theorem proving, make it more convenient and truly interactive! arend-lang.github.io/documentation/…

Arend 1.8 is released! Improved performance and a convenient syntax for HITs, proof search and step-by-step type-checking. The standard library received a huge update too. For more information, see arend-lang.github.io/2022/04/15/Are….

Arend 1.9 is released. In the new version, we added infix patterns and a convenient mechanism for showing implicit arguments and other info in error messages. The standard library now has real numbers and schemes. For more info, see arend-lang.github.io/2022/12/04/Are….

Arend 1.10 is released. This release provides a massive update to the standard library, which includes topics in linear algebra, field theory, topology, and analysis. For more information, see arend-lang.github.io/2024/07/05/Are…