More Like this

1. Metrical properties of functions of consecutive digits in Lüroth series

   Kleinbock, Dmitry; Zhang, Yuqing (July 2024, Integers)

   Recently, the growth of the products of L¨uroth quotients d_i(x) in the L¨uroth expansion of a real number x was studied in connection with improvements to Dirichlet’s theorem. 

   more » « less
2. Diversity-Driven Automated Formal Verification

   https://doi.org/10.1145/3510003.3510138  

   First, Emily; Brun, Yuriy (May 2022, Proceedings of the 44th International Conference on Software Engineering (ICSE))

   Formally verified correctness is one of the most desirable properties of software systems. But despite great progress made via interactive theorem provers, such as Coq, writing proof scripts for verification remains one of the most effort-intensive (and often prohibitively difficult) software development activities. Recent work has created tools that automatically synthesize proofs or proof scripts. For example, CoqHammer can prove 26.6% of theorems completely automatically by reasoning using precomputed facts, while TacTok and ASTactic, which use machine learning to model proof scripts and then perform biased search through the proof-script space, can prove 12.9% and 12.3% of the theorems, respectively. Further, these three tools are highly complementary; together, they can prove 30.4% of the theorems fully automatically. Our key insight is that control over the learning process can produce a diverse set of models, and that, due to the unique nature of proof synthesis (the existence of the theorem prover, an oracle that infallibly judges a proof's correctness), this diversity can significantly improve these tools' proving power. Accordingly, we develop Diva, which uses a diverse set of models with TacTok's and ASTactic's search mechanism to prove 21.7% of the theorems. That is, Diva proves 68% more theorems than TacTok and 77% more than ASTactic. Complementary to CoqHammer, Diva proves 781 theorems (27% added value) that Coq-Hammer does not, and 364 theorems no existing tool has proved automatically. Together with CoqHammer, Diva proves 33.8% of the theorems, the largest fraction to date. We explore nine dimensions for learning diverse models, and identify which dimensions lead to the most useful diversity. Further, we develop an optimization to speed up Diva's execution by 40X. Our study introduces a completely new idea for using diversity in machine learning to improve the power of state-of-the-art proof-script synthesis techniques, and empirically demonstrates that the improvement is significant on a dataset of 68K theorems from 122 open-source software projects. 

   more » « less
3. On the local converse theorem for split 𝑆𝑂_{2𝑙}

   https://doi.org/10.1090/ert/687  

   Hazeltine, Alexander; Liu, Baiying (March 2025, Representation Theory)

   In this paper, we prove the local converse theorem for split even special orthogonal groups over a non-Archimedean local field of characteristic $p\ne <\#comment/>2$. This is the only case left on local converse theorems of split classical groups and the difficulty is the existence of the outer automorphism. We apply a new idea by considering a certain sum of partial Bessel functions to overcome this difficulty. As a direct application, we obtain a weak rigidity theorem for irreducible generic cuspidal representations of split even special orthogonal groups. 

   more » « less
4. 2d $$ \mathcal{N} $$ = (0, 1) gauge theories and Spin(7) orientifolds

   https://doi.org/10.1007/JHEP03(2022)150  

   Franco, Sebastián; Mininno, Alessandro; Uranga, Ángel M.; Yu, Xingyang (March 2022, Journal of High Energy Physics)

   A bstract We initiate the geometric engineering of 2d $$ \mathcal{N} $$ N = (0 , 1) gauge theories on D1-branes probing singularities. To do so, we introduce a new class of backgrounds obtained as quotients of Calabi-Yau 4-folds by a combination of an anti-holomorphic involution leading to a Spin(7) cone and worldsheet parity. We refer to such constructions as Spin(7) orientifolds . Spin(7) orientifolds explicitly realize the perspective on 2d $$ \mathcal{N} $$ N = (0 , 1) theories as real slices of $$ \mathcal{N} $$ N = (0 , 2) ones. Remarkably, this projection is geometrically realized as Joyce’s construction of Spin(7) manifolds via quotients of Calabi-Yau 4-folds by anti-holomorphic involutions. We illustrate this construction in numerous examples with both orbifold and non-orbifold parent singularities, discuss the role of the choice of vector structure in the orientifold quotient, and study partial resolutions. 

   more » « less
5. Quantitative finiteness of hyperplanes in hybrid manifolds

   Ohm, Ko; Sanchez, Anthony (June 2025, arXiv)

   We prove a quantitative finiteness theorem for the number of totally geodesic hyperplanes of non-arithmetic hyperbolic n-manifolds that arise from a gluing construction of Gromov and Piatetski-Shapiro for n ≥ 3. This extends work of LindenstraussMohammadi in dimension 3. This follows from effective density theorem for periodic orbits of SO(n −1,1) acting on quotients of SO(n,1) by a lattice for n ≥ 3. The effective density result uses a number of a ideas including Margulis functions, a restricted projection theorem, and an effective equidistribution result for measures on the horospherical subgroup that are nearly full dimensional. 

   more » « less