ELTE project among Europe's leading discovery research
The European Research Council (ERC) rewards the most promising research from discovery to the early exploitation phase of the Horizon Europe programme. The Consolidator Grant scheme recognises research with an established team and outstanding results that show promise of scientific breakthrough.
Ambrus Kaposi and his team with their research on Higher Observational Type Theory (HOTT)
could revolutionise the use of computer-based proof systems.
Computer proof checkers are based on type theory. Type theory is a formal language for doing high assurance computer programming and for checking the correctness of mathematical proofs. The type of a program is the statement itself, and the program corresponding to the type is the proof of the statement.
In higher-dimensional models of type theory, the elements of types are given by points in an abstract space, and elements of the equality type are given by the paths between points. Building on such models, homotopy type theory was developed, which justify the principle that isomorphic types are equal. This principle brings computational proofs close to everyday mathematical practice, where isomorphic structures are considered to be identical.
The HOTT project aims to develop a new version of homotopy type theory in which higher-dimensional geometry is not manually incorporated but emergent. The basic idea is that the equality type is not given geometrically but via computation. This makes homotopy type theory explainable and shortens the proofs, since parts of the proofs become automatic computations. In the long run, our new type theory will contribute to the development of computer verification of mathematical proofs and to the development of provably correct software by allowing abstract, reusable proofs.
