JetBrains/Arend

The Arend Proof Assistant

Source code at GitHub https://arend-lang.github.io/

{
  "createdAt": "2015-02-16T12:07:33Z",
  "defaultBranch": "master",
  "description": "The Arend Proof Assistant",
  "fullName": "JetBrains/Arend",
  "homepage": "https://arend-lang.github.io/",
  "language": "Java",
  "name": "Arend",
  "pushedAt": "2025-02-25T11:07:38Z",
  "stargazersCount": 735,
  "topics": [
    "arend"
  ],
  "updatedAt": "2025-11-23T23:27:42Z",
  "url": "https://github.com/JetBrains/Arend"
}

Arend proof assistant

Arend is a theorem prover and a programming language based on Homotopy Type Theory.

For more information about the Arend language, visit arend-lang.github.io or the documentation.
For instructions on building Arend locally, general description of the codebase, there’s [ARCHITECTURE.md]!(ARCHITECTURE.md).
For community forums, checkout this link.
For editing Arend code, we suggest IntelliJ Arend (instructions).
The standard library of Arend is here. It serves as a math library.

Usage

As a binary

You can find release version of Arend binary (a jar file named “Arend.jar”) in the release page. The Arend jar can be used to typecheck a library:

$ java -jar Arend.jar [path-to-library]

You can also start a REPL:

$ java -jar Arend.jar -i

If you start the REPL at the root directory of a library, the REPL will load the library. For more information and usage about command line usage of Arend, please refer to --help:

$ java -jar Arend.jar -h

As a library

Arend is under active development, so you may expect to depend your project on a development version of Arend, either a certain git revision or the SNAPSHOT version. This is possible via JitPack, simply add this to your build.gradle:

repositories {
    maven { url 'https://jitpack.io' }
}
dependencies {
    // The version of Arend -- can be a short revision, "[branch]-SNAPSHOT",
    // "-SNAPSHOT", or a tag (or a release, like "v1.4.0").
    String arendVersion = "master-SNAPSHOT"
    // Open API for writing Arend extensions
    implementation "com.github.JetBrains.Arend:api:$arendVersion"
    // The generated ANTLR parser
    implementation "com.github.JetBrains.Arend:parser:$arendVersion"
    // The generated protobuf classes
    implementation "com.github.JetBrains.Arend:proto:$arendVersion"
    // The main compiler
    implementation "com.github.JetBrains.Arend:base:$arendVersion"
}

In case you prefer Gradle Kotlin DSL, use the following syntax in your build.gradle.kts:

repositories {
    maven("https://jitpack.io")
}
dependencies {
    // The version of Arend
    val arendVersion = "master-SNAPSHOT"
    implementation("com.github.JetBrains.Arend:api:$arendVersion")
    implementation("com.github.JetBrains.Arend:parser:$arendVersion")
    implementation("com.github.JetBrains.Arend:proto:$arendVersion")
    implementation("com.github.JetBrains.Arend:base:$arendVersion")
}