# The Aya Prover

Aya is a programming language and a proof assistant designed for formalizing math and type-directed programming.

The type system of Aya features in homotopical features similar to Arend (opens new window), overlapping but confluent pattern matching, and abstraction over definitional equalities.

Aya is under active development. Please be patient until future information is available.