What is Hackers' Pub?

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can be composed. We show that all higher coherences can be stated and derived if simplicial type theory is taken to be homotopy type theory with a postulated interval type. In technical terms, this means that if a type has unique fillers for $(2,1)$-horns, it has unique fillers for all inner $(n,k)$-horns. This generalizes a result of Riehl and Shulman for the case $n = 3, k \in \{1, 2\}$. Our main technical tool is the Leibniz adjunction: the pushout-product is left adjoint to the pullback-hom in the wild category of types. While this adjunction is well known for ordinary categories, it is much more involved for higher categories, and the fact that it can be proved for the wild category of types (a higher category without stated higher coherences) is non-trivial. We make profitable use of the equivalence between the wild category of maps and that of families. We have formalized the results in Cubical Agda.

arxiv.org · arXiv.org

Formalization of non-Archimedean functional analysis 1: spherically complete spaces

In this article, we present a formalization of spherically complete spaces, which is a fundamental notion in non-archimedean functional analysis. This work includes the equivalent definitions of spherically complete spaces, their basic properties, examples and non-examples such as the field $\mathbf{C}_p$ of $p$-adic complex numbers. As applications, we formalize the Birkhoff-James orthogonality, Hahn-Banach extension theorem and the spherical completion for non-archimedean Banach spaces. Code available at https://github.com/YijunYuan/SphericalCompleteness

arxiv.org · arXiv.org

Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the Erdős Problems

We present a case study in semi-autonomous mathematics discovery, using Gemini to systematically evaluate 700 conjectures labeled 'Open' in Bloom's Erdős Problems database. We employ a hybrid methodology: AI-driven natural language verification to narrow the search space, followed by human expert evaluation to gauge correctness and novelty. We address 13 problems that were marked 'Open' in the database: 5 through seemingly novel autonomous solutions, and 8 through identification of previous solutions in the existing literature. Our findings suggest that the 'Open' status of the problems was through obscurity rather than difficulty. We also identify and discuss issues arising in applying AI to math conjectures at scale, highlighting the difficulty of literature identification and the risk of ''subconscious plagiarism'' by AI. We reflect on the takeaways from AI-assisted efforts on the Erdős Problems.

arxiv.org · arXiv.org

Recent Advances in LLMs for Mathematics

I review the progress of large language models for mathematics over the last 3 years, from barely solving high school level mathematics to solving some minor...

www.youtube.com · YouTube

CIS352

CMSC352--Principles of Programming Languages (Spring '26) at Syracuse

kmicinski.com

Mechanized Undecidability of Higher-order beta-Matching (Extended Version)

Higher-order beta-matching is the following decision problem: given two simply typed lambda-terms, can the first term be instantiated to be beta-equivalent to the second term? This problem was formulated by Huet in the 1970s and shown undecidable by Loader in 2003 by reduction from lambda-definability. The present work provides a novel undecidability proof for higher-order beta-matching, in an effort to verify this result by means of a proof assistant. Rather than starting from lambda-definability, the presented proof encodes a restricted form of string rewriting as higher-order beta-matching. The particular approach is similar to Urzyczyn's undecidability result for intersection type inhabitation. The presented approach has several advantages. First, the proof is simpler to verify in full detail due to the simple form of rewriting systems, which serve as a starting point. Second, undecidability of the considered problem in string rewriting is already certified using the Coq proof assistant. As a consequence, we obtain a certified many-one reduction from the Halting Problem to higher-order beta-matching. Third, the presented approach identifies a uniform construction which shows undecidability of higher-order beta-matching, lambda-definability, and intersection type inhabitation. The presented undecidability proof is mechanized in the Coq proof assistant and contributed to the existing Coq Library of Undecidability Proofs.

arxiv.org · arXiv.org

LeanArchitect: Automating Blueprint Generation for Humans and AI

Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are central to human collaboration, existing tooling treats the informal ($\LaTeX$) and formal (Lean) components as largely decoupled artifacts, leading to maintenance overhead and limiting integration with AI automation. We present LeanArchitect, a Lean package for extracting, managing, and exporting blueprint data directly from Lean code. LeanArchitect introduces a declarative annotation mechanism that associates formal declarations with blueprint metadata, automatically infers dependency information, and generates $\LaTeX$ blueprint content synchronized with the Lean development. This design eliminates duplication between formal and informal representations and eases fine-grained progress tracking for both human contributors and AI-based theorem provers. We demonstrate the practicality of LeanArchitect through the automated conversion of several large existing blueprint-driven projects, and through a human--AI collaboration case study formalizing a multivariate Taylor theorem. Our results show that LeanArchitect improves maintainability, exposes latent inconsistencies in existing blueprints, and provides an effective interface for integrating AI tools into real-world formalization workflows.

arxiv.org · arXiv.org

Irrationality of rapidly converging series: a problem of Erdős and Graham

Answering a question of Erdős and Graham, we show that the double exponential growth condition $\limsup_{n\to\infty}a_n^{1/ϕ^n}=\infty$ for a strictly increasing sequence of positive integers $\{a_n\}_{n=1}^\infty$ is sufficient for the series $\sum_{n=1}^\infty 1/(a_n a_{n+1})$ to have an irrational sum; here $ϕ$ denotes the golden ratio. We also provide a positive generalization to $\sum_{n=1}^\infty 1/(a_n^{w_0}\cdots a_{n+d-1}^{w_{d-1}})$, and a negative result showing that some of its instances are essentially optimal. The original problem was autonomously solved by the AI agent \emph{Aletheia}, powered by Gemini Deep Think, while the remaining material is largely a product of human-AI interactions.

arxiv.org · arXiv.org

Flow-based Extremal Mathematical Structure Discovery

The discovery of extremal structures in mathematics requires navigating vast and nonconvex landscapes where analytical methods offer little guidance and brute-force search becomes intractable. We introduce FlowBoost, a closed-loop generative framework that learns to discover rare and extremal geometric structures by combining three components: (i) a geometry-aware conditional flow-matching model that learns to sample high-quality configurations, (ii) reward-guided policy optimization with action exploration that directly optimizes the generation process toward the objective while maintaining diversity, and (iii) stochastic local search for both training-data generation and final refinement. Unlike prior open-loop approaches, such as PatternBoost that retrains on filtered discrete samples, or AlphaEvolve which relies on frozen Large Language Models (LLMs) as evolutionary mutation operators, FlowBoost enforces geometric feasibility during sampling, and propagates reward signal directly into the generative model, closing the optimization loop and requiring much smaller training sets and shorter training times, and reducing the required outer-loop iterations by orders of magnitude, while eliminating dependence on LLMs. We demonstrate the framework on four geometric optimization problems: sphere packing in hypercubes, circle packing maximizing sum of radii, the Heilbronn triangle problem, and star discrepancy minimization. In several cases, FlowBoost discovers configurations that match or exceed the best known results. For circle packings, we improve the best known lower bounds, surpassing the LLM-based system AlphaEvolve while using substantially fewer computational resources.

arxiv.org · arXiv.org

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4

Recent advances in large language models have demonstrated impressive capabilities in mathematical formalization. However, existing benchmarks focus on logical verification of declarative propositions, often neglecting the task of explicitly synthesizing solutions. This limitation is particularly acute in applied mathematics domains, where the goal is frequently to derive concrete values or executable algorithms rather than solely proving theorems. To address this, we introduce a Lean 4 framework that enforces a construction-verification workflow, compelling the agent to define explicit solutions before proving their correctness. We curate a comprehensive benchmark AMBER (Applied Mathematics BEnchmark for Reasoning) spanning core domains of applied mathematics, including convex analysis, optimization, numerical algebra, and high-dimensional probability. Aside from theorem proving, our benchmark features complex tasks such as evaluation, algorithm design, and representation transformation. Experiments reveal that current models face significant difficulties with these constructive tasks. Notably, we observe that general-purpose reasoning models consistently outperform specialized theorem provers. We attribute this to a degradation of instruction following capabilities in specialized models. Fine-tuning on proof corpora appears to induce ``tactical overfitting", compromising the ability to adhere to complex constructive requirements, whereas general models retain the versatility needed for multi-task formal reasoning.

arxiv.org · arXiv.org

Emily Riehl — The future of mathematics | Math, Inc.

Emily Riehl sits down with Math Inc's Jesse Han and Jared Duker Lichtman for a conversation on the future of mathematics.Riehl is a distinguished Professor o...

www.youtube.com · YouTube

10년간 본회의 고작 18번…‘유명무실’ 양성평등위 개편

정부가 ‘양성평등위원회’(양평위) 개편에 나섰다. 양평위는 양성평등기본법에 따라 국무총리가 주재하는 범정부 성평등 정책 심의·조정 기구다. 출범 10년을 넘겼으나 “그런 게 있었나?” 반응이 나올 정도로 존재감이 약해, 그동안의 형식적 운영에서 벗어나 실질적인 ‘성평등

www.hani.co.kr · 한겨레

Open Net Files Constitutional Complaint Challenging Ban on Political Activities by Foreign Nationals

On January 28, 2026, Open Net, together with Law Firm Innovation (attorneys Jiwon Son and Jihwan Park), filed a constitutional complaint seeking a declaration of unconstitutionality of Article 17(2) of the Immigration Control Act, commonly referred to as the “ban on political activities by foreign n

www.opennetkorea.org · OPEN NET