1. Outstanding basic research outcome
Automorphic Forms Lendület Research Group
Automorphic forms are harmonic waves with a rich symmetry, and the various harmonies are encoded by L-functions (the most classical L-function is the Riemann zeta function, fundamental in prime number theory). Many famous and extremely difficult problems are concerned with these objects (e.g. the generalized Riemann hypothesis, the Ramanujan-Selberg conjecture, the Langlands program), and number theory is connected to several seemingly distant mathematical areas through these objects (e.g. representation theory of Lie groups, global analysis, mathematical physics). In recent years, numerous Fields medals were awarded for the research of automorphic forms: Vladimir Drinfeld (1990), Richard Borcherds (1998), Laurent Lafforgue (2002), Ngô Bao Châu (2010), Elon Lindenstrauss (2010), Peter Scholze (2018), Akshay Venkatesh (2018).
A Maass form
A central theme of modern analytic number theory is the estimation of automorphic forms in various families in various norms. Such estimates are needed in concrete applications, but they also play a leading role in the development of the theory. The most classical automorphic forms are functions of the algebraic groups GL(1) and GL(2) over the adele ring of various number fields – these have been studied for over a century and a half. It is a logical step to extend the existing results to the groups GL(n) of higher rank, but despite intensive research efforts, there are few general theorems. Hence it was all the more surprising when Blomer-Maga (2014) managed to give a nontrivial pointwise bound for every spherical Hecke-Maass form on a fixed compact subset of the group PGL(n) over the rational numbers. Around the same time, Brumley-Templier (2014) showed that the restriction to compact subsets is essential, because without it the automorphic form assumes much larger values. Within the framework of the Automorphic Forms Momentum Grant, Blomer-Harcos-Maga [1, 2] proved that the lower bound of Brumley-Templier (2014) is close to the truth, because an upper bound of similar shape is also valid. On the classical group PGL(2), Blomer-Harcos-Maga-Milićević  established a strong and general bound, which concerns every number field and non-spherical forms, too. This theorem generalizes and sharpens several earlier results, such as the bound of Blomer-Harcos-Milićević (2016) on arithmetic hyperbolic 3-manifolds. The new results were accepted for publication by first-rate journals – after a lengthy review process as customary in mathematics.
-  Blomer V, Harcos G, Maga P: Analytic properties of spherical cusp forms on GL(n), JOURNAL D ANALYSE MATHEMATIQUE (2020) REAL arXiv
-  Blomer V, Harcos G, Maga P: On the global sup-norm of GL(3) cusp forms, ISRAEL JOURNAL OF MATHEMATICS 229 : 1 pp. 357-379., 23 p. (2019) DOI REALMathematical Reviews WoS Scopus arXiv
-  Blomer V, Harcos G, Maga P, Milićević D: The sup-norm problem for GL(2) over number fields, JOURNAL OF THE EUROPEAN MATHEMATICAL SOCIETY 22 : 1 pp. 1-53., 53 p. (2020) DOI REAL Egyéb URL arXiv
2. Outstanding applied research outcome
Artificial Intelligence Research Group
Automated Theorem Proving (ATP) and Deep Learning (DL) are two important branches of artificial intelligence both of which have undergone huge development over the past decade. A novel and exciting research direction is to find a synthesis of these two domains. One possible approach is to use an intelligent learning system to guide the theorem prover as it explores the search space of possible derivations. The research group of the Institute tackled the question of how to generalize from short proofs to longer ones with a strongly related structure. This is an important task since proving interesting problems typically requires thousands of steps, while current ATP methods are only finding proofs that are at most a couple dozens of steps long. The project has a homepage (http://bit.ly/site_atpcurr) and a public code repository (http://bit.ly/code_atpcurr). This work has been presented at the Bumerang Workshop, the Conference on Artificial Intelligence and Theorem Proving the Dagstuhl Logic and Learning Seminar and the NeurIPS 2019 workshop Knowledge Representation Meets Machine Learning (KR2ML2019). A paper about this project is currently under review.
- Zombori Zs, Csiszárik A, Michalewski H, Kaliszyk C, Urban J: Towards Finding Longer Proofs (2019) arXiv
The group has built a system, called FLoP that searches for proofs using reinforcement learning. FLoP has been tested using a set of simple arithmetic theorems, which has many convenient properties for comparing machine learning methods: proofs are long (even thousands of steps) and repetitive, however, they often share a general structure. Despite their apparent simplicity, these arithmetic problems are already hard for the strongest automated theorem proving systems (E, Vampire), mostly due to the length of the proofs. The chart below compares our system (FLoP) with other methods that rely on search space exploration. FLoP performs reasonably well on these datasets.