# AI for Mathematics & Formal Proof Domain: Mathematics & Theoretical Computer Science · 244 papers indexed · newest 2026-10-29 Lean and Mathlib, autoformalization, neural theorem proving, olympiad-level systems and AI-assisted discovery in mathematics. Key concepts: theorem proving, Lean, autoformalization, formal mathematics, mathematical reasoning, olympiad ## Most influential - **[Self-Normalizing Neural Networks](https://space-kitty.com/papers/arxiv:1706.02515)**. Günter Klambauer, Thomas Unterthiner, Andreas Mayr et al. · 2017 · Advances in Neural Information Processing Systems 30 (NIPS 2017) (arXiv:1706.02515 · 2,031 citations). Source: > Deep Learning has revolutionized vision via convolutional neural networks (CNNs) and natural language processing via recurrent neural networks (RNNs). However, success stories of Deep Learning with standard feed-forward neural networks (FNNs) are rare. FNNs that perform well are typically shallow and, therefore cannot exploit many levels of abstract representations. We introduce self-normalizing neural networks (SNNs) to enable high-level abstract representations. While batch normalization requires explicit normalization, neuron activations of SNNs automatically converge towards zero mean and … - **[Solving olympiad geometry without human demonstrations](https://space-kitty.com/papers/doi:10.1038/s41586-023-06747-5)**. Trieu H. Trinh, Yuhuai Wu, Quoc Viet Le et al. · 2024 · Nature (doi:10.1038/s41586-023-06747-5 · 311 citations). Source: > Abstract Proving mathematical theorems at the olympiad level represents a notable milestone in human-level automated reasoning 1–4 , owing to their reputed difficulty among the world’s best talents in pre-university mathematics. Current machine-learning approaches, however, are not applicable to most mathematical domains owing to the high cost of translating human proofs into machine-verifiable format. The problem is even worse for geometry because of its unique translation challenges 1,5 , resulting in severe scarcity of training data. We propose AlphaGeometry, a theorem prover for Euclidean … > _Abstract excerpt by Trieu H. Trinh et al., CC-BY, https://doi.org/10.1038/s41586-023-06747-5; truncated._ - **[The expressive power of neural networks: a view from the width](https://space-kitty.com/papers/openalex:W2963097630)**. Lu Zhou, Hongming Pu, Feicheng Wang et al. · 2017 · neural information processing systems (516 citations). Source: - **[Direct Adaptive Neural Control for a Class of Uncertain Nonaffine Nonlinear Systems Based on Disturbance Observer](https://space-kitty.com/papers/doi:10.1109/tsmcb.2012.2226577)**. Mou Chen, Shuzhi Sam Ge · 2012 · IEEE Transactions on Cybernetics (doi:10.1109/tsmcb.2012.2226577 · 396 citations). Source: - **[Convergence Analysis of Two-layer Neural Networks with ReLU Activation](https://space-kitty.com/papers/arxiv:1705.09886)**. Yuanzhi Li, Yuan Yang · 2017 (arXiv:1705.09886 · 304 citations). Source: > In recent years, stochastic gradient descent (SGD) based techniques has become the standard tools for training neural networks. However, formal theoretical understanding of why SGD can train neural networks in practice is largely missing. In this paper, we make progress on understanding this mystery by providing a convergence analysis for SGD on a rich subset of two-layer feedforward networks with ReLU activations. This subset is characterized by a special structure called "identity mapping". We prove that, if input follows from Gaussian distribution, with standard $O(1/\\sqrt{d})$ initializati… - **[Theory of deep convolutional neural networks: Downsampling](https://space-kitty.com/papers/doi:10.1016/j.neunet.2020.01.018)**. Ding‐Xuan Zhou · 2020 · Neural Networks (doi:10.1016/j.neunet.2020.01.018 · 263 citations). Source: - **[Neural Operator: Learning Maps Between Function Spaces](https://space-kitty.com/papers/arxiv:2108.08481)**. Nikola Kovachki, Zongyi Li, Burigede Liu et al. · 2021 · The Journal of Machine Learning Research (2023), Volume 24, Issue 1, Article No 89, pp 4061-4157 (arXiv:2108.08481 · doi:10.5555/3648699.3648788 · 217 citations). Source: > The classical development of neural networks has primarily focused on learning mappings between finite dimensional Euclidean spaces or finite sets. We propose a generalization of neural networks to learn operators, termed neural operators, that map between infinite dimensional function spaces. We formulate the neural operator as a composition of linear integral operators and nonlinear activation functions. We prove a universal approximation theorem for our proposed neural operator, showing that it can approximate any given nonlinear continuous operator. The proposed neural operators are also d… - **[Global stability analysis of fractional-order Hopfield neural networks with time delay](https://space-kitty.com/papers/doi:10.1016/j.neucom.2014.12.031)**. Wang Hu, Yongguang Yu, Guoguang Wen et al. · 2014 · Neurocomputing (doi:10.1016/j.neucom.2014.12.031 · 258 citations). Source: - **[Adaptive Neural Backstepping Control Design for A Class of Nonsmooth Nonlinear Systems](https://space-kitty.com/papers/doi:10.1109/tsmc.2018.2875947)**. Xudong Zhao, Xinyong Wang, Shuo Zhang et al. · 2018 · IEEE Transactions on Systems Man and Cybernetics Systems (doi:10.1109/tsmc.2018.2875947 · 208 citations). Source: - **[Recurrent Neural Network for Non-Smooth Convex Optimization Problems With Application to the Identification of Genetic Regulatory Networks](https://space-kitty.com/papers/doi:10.1109/tnn.2011.2109735)**. Long Cheng, Zeng‐Guang Hou, Yingzi Lin et al. · 2011 · IEEE Transactions on Neural Networks (doi:10.1109/tnn.2011.2109735 · 213 citations). Source: - **[Neuro-symbolic approaches in artificial intelligence](https://space-kitty.com/papers/doi:10.1093/nsr/nwac035)**. Pascal Hitzler, Aaron Eberhart, Monireh Ebrahimi et al. · 2022 · National Science Review (doi:10.1093/nsr/nwac035 · 167 citations). Source: > Neuro-symbolic artificial intelligence refers to a field of research and applications that combines machine learning methods based on artificial neural networks, such as deep learning, with symbolic approaches to computing and artificial intelligence (AI), as can be found for example in the AI subfield of knowledge representation and reasoning. Neuro-symbolic AI has a long history; however, it remained a rather niche topic until recently, when landmark advances in machine learning—prompted by deep learning—caused a significant rise in interest and research activity in combining neural and symb… > _Abstract excerpt by Pascal Hitzler et al., CC-BY, https://doi.org/10.1093/nsr/nwac035; truncated._ - **[Adaptive Neural Network Output Feedback Control for Stochastic Nonlinear Systems With Unknown Dead-Zone and Unmodeled Dynamics](https://space-kitty.com/papers/doi:10.1109/tcyb.2013.2276043)**. Shaocheng Tong, Tong Wang, Yongming Li et al. · 2014 · IEEE Transactions on Cybernetics (doi:10.1109/tcyb.2013.2276043 · 204 citations). Source: - **[Convergence Analysis of Two-layer Neural Networks with ReLU Activation](https://space-kitty.com/papers/openalex:W2963519230)**. Yuanzhi Li, Yuan Yang · 2017 · neural information processing systems (192 citations). Source: - **[Neural Network Learning Adaptive Robust Control of an Industrial Linear Motor-Driven Stage With Disturbance Rejection Ability](https://space-kitty.com/papers/doi:10.1109/tii.2017.2684820)**. Ze Wang, Chuxiong Hu, Yu Zhu et al. · 2017 · IEEE Transactions on Industrial Informatics (doi:10.1109/tii.2017.2684820 · 177 citations). Source: - **[Universal Approximations of Invariant Maps by Neural Networks](https://space-kitty.com/papers/arxiv:1804.10306)**. Dmitry Yarotsky · 2021 · Constructive Approximation (arXiv:1804.10306 · doi:10.1007/s00365-021-09546-1 · 139 citations). Source: > We describe generalizations of the universal approximation theorem for neural networks to maps invariant or equivariant with respect to linear representations of groups. Our goal is to establish network-like computational models that are both invariant/equivariant and provably complete in the sense of their ability to approximate any continuous invariant/equivariant map. Our contribution is three-fold. First, in the general case of compact groups we propose a construction of a complete invariant/equivariant network using an intermediate polynomial layer. We invoke classical theorems of Hilbert… ## Newest - **[RetroChessBench: A Benchmark for Reconstructing and Proving Chess Histories](https://space-kitty.com/papers/arxiv:2610.39341)**. Tidor-Vlad Pricope · 2026 (arXiv:2610.39341). Source: - **[Construction and formal verification of a special topology on {\\mathbb{Z}}^{n}: characterization of connected subsets](https://space-kitty.com/papers/arxiv:2610.39354)**. Ignacio Vega-Páez · 2026 (arXiv:2610.39354). Source: - **[Semantic Path Orders are Generalized Weighted Path Orders](https://space-kitty.com/papers/arxiv:2610.39536)**. Teppei Saito, Nao Hirokawa · 2026 (arXiv:2610.39536). Source: - **[Countable Nondeterminism in Weighted Programming with an Application to Mechanized Foundations for Probabilistic Program Verification](https://space-kitty.com/papers/arxiv:2610.39723)**. Sebastian Körner, Oliver Emil Bøving, Christoph Matheja · 2026 (arXiv:2610.39723). Source: - **[H$^2$R: Hierarchical Hint-Based Reward for Mathematical Reasoning via Reinforcement Learning](https://space-kitty.com/papers/arxiv:2610.39934)**. He Tu, Siye Li, Hongyi Wen · 2026 (arXiv:2610.39934). Source: - **[The generative paradox: the Anti-Prompt paradigm for human capability](https://space-kitty.com/papers/arxiv:2610.40151)**. Margarita Trifonov Vadim E. Levit · 2026 (arXiv:2610.40151). Source: - **[Hammering with Vampire in Lean](https://space-kitty.com/papers/arxiv:2610.40310)**. Jonas Bodingbauer, Laura Kovács · 2026 (arXiv:2610.40310). Source: - **[Scaling Mathematical Proof Supervision from Structured Textbooks](https://space-kitty.com/papers/arxiv:2610.40394)**. Youqing Fang, Zhouqi Hua, Yinhao Tang et al. · 2026 (arXiv:2610.40394). Source: - **[Algebraic World Model: From Exploration to Proofs](https://space-kitty.com/papers/arxiv:2610.40503)**. Guancheng Pan, Qixin Tan, Yang Yuan et al. · 2026 (arXiv:2610.40503). Source: - **[crush: Extensible Proof Automation for Lean](https://space-kitty.com/papers/arxiv:2610.40538)**. Mike He, Dexin Zhang, Aarti Gupta · 2026 (arXiv:2610.40538). Source: --- Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.