Arend Proof Assistant is a next-generation proof assistant developed at JetBrains based on the homotopy-type theory. The aim of the proposed project is to improve the tooling for the Arend Proof Assistant, namely to develop a "bounded proof search" tactic, which would facilitate development of proofs in Arend.

Applicant must meet the following criteria:

• have at least a BSc degree in mathematics or computer science;

• be acquainted with Java/Kotlin development;

• have some knowledge of mathematical logic (type theory, first-order-logic), know how the resolution algorithm works.