https://arxiv.org/api/voqV6tZth8ZhqRr7Ra0/efAFQL8 2026-03-22T11:51:50Z 15279 30 15 http://arxiv.org/abs/2603.15929v1 2026-03-16T21:21:53Z

We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project demonstrates the full AI-assisted mathematical research loop: an AI reasoning model (Gemini DeepThink) generated the proof from a conjecture, an agentic coding tool (Claude Code) translated it into Lean from natural-language prompts, a specialized prover (Aristotle) closed 111 lemmas, and the Lean kernel verified the result. A single mathematician supervised the process over 10 days at a cost of \$200, writing zero lines of code. The entire development process is public: all 229 human prompts, and 213 git commits are archived in the repository. We report detailed lessons on AI failure modes -- hypothesis creep, definition-alignment bugs, agent avoidance behaviors -- and on what worked: the abstract/concrete proof split, adversarial self-review, and the critical role of human review of key definitions and theorem statements. Notably, the formalization was completed before the final draft of the corresponding math paper was finished.

2026-03-16T21:21:53Z 11 figures Vasily Ilin http://arxiv.org/abs/2204.05900v7 2026-03-16T18:14:34Z

In this paper, we establish a theorem on extension of Lipschitz maps $f$ definable in Hensel minimal, non-trivially valued fields $K$ of equicharacteristic zero. This may be regarded as a definable, non-Archimedean, non-locally compact version of Kirszbraun's extension theorem. We proceed with double induction with respect to the dimensions of the ambient space and of the domain of $f$. To this end, we introduce the concept of a definable open cell package with a skeleton which, along with the concept of a risometry, plays a key role in our induction procedure.

2022-04-12T15:53:59Z Some comments added Krzysztof Jan Nowak http://arxiv.org/abs/2412.16071v4 2026-03-16T17:42:17Z

Cummings, Foreman, and Magidor investigated the extent to which square principles are compact at singular cardinals. The first author proved that if $κ$ is a singular strong limit of uncountable cofinality, all scales on $κ$ are good, and $\square^*_δ$ holds for all $δ<κ$, then $\square_κ^*$ holds. In this paper we will present a strongly contrasting result for $\aleph_ω$. We construct a model in which $\square_{\aleph_n}$ holds for all $n<ω$, all scales on $\aleph_ω$ are good, but in which $\square_{\aleph_ω}^*$ fails and some weak forms of internal approachability for $[H(\aleph_{ω+1})]^{\aleph_1}$ fail. This requires an extensive analysis of the dominating and approximation properties of a version of Namba forcing. We also prove some supporting results.

2024-12-20T17:12:59Z Tentative update submitted in September 2025 Maxwell Levine Heike Mildenberger http://arxiv.org/abs/2209.12258v2 2026-03-16T17:35:52Z

We introduce a forcing that adds a $\square(\aleph_2,\aleph_0)$-sequence with countable conditions under CH. Assuming the consistency of a weakly compact cardinal, we can find a forcing extension by our new poset in which both $\square(\aleph_2,<\!\aleph_0)$ and $\square_{\aleph_1,\aleph_0}$ fail in the forcing extension.

2022-09-25T16:28:13Z Tentative revision; more revisions are still needed, in particular for Section 3 Maxwell Levine http://arxiv.org/abs/2601.14029v2 2026-03-16T13:54:15Z

Causality is one of the fundamental structures of spacetimes, determining the possible behaviour and propagation of physical information. Causal structure can be analysed through the various modal logics it induces. The modal logics for the chronological and causal relations of the archetypal Minkowski spacetime have been classified. However, only partial results have been achieved for the strict variant of the causal relation, known as the after relation. Towards classification, it was shown by Shapirovsky and Shehtman that the after modality in Minkowski space satisfies a formula we call the 'after formula'. The present work continues this analysis towards arbitrary spacetimes. In particular, we prove that the after modality in any smooth spacetime satisfies the after formula. We introduce a related modal formula that demonstrates that the logic of two-dimensional spacetimes are more expressive than higher-dimensional ones. Lastly, we study the interrelation between the logical properties and physical properties along the causal ladder.

2026-01-20T14:53:16Z 31 pages, 16 figures; fixed proof of main theorem in Section 4, other minor changes Marco Lewis Nesta van der Schaaf http://arxiv.org/abs/2404.04976v6 2026-03-16T13:53:26Z

Let $L$ be the language of rings. We provide an axiomatization of the $L$-theories of quaternions and octonions and characterize their models: they coincide, up to isomorphism, with quaternion and octonion algebras over a real closed field, respectively. We bi-interpret these theories in terms of real closed fields and we prove they are complete, model complete and they do not have quantifier elimination. Then, we focus on the class of ordered polynomials. Over $\mathbb{H}$ and $\mathbb{O}$ these polynomials are of special interest in hypercomplex analysis since they are slice regular. We deduce some fundamental properties of their zero loci from model completeness and we introduce the notions of algebraic sets and Zariski topology. Finally, we prove the failure of quantifier elimination for the fragment of ordered formulas and we completely characterize the family of algebraic sets.

2024-04-07T14:35:17Z We added some results concerning algebraic sets and the Zariski topology over quaternions and ocronions. Updated references. This is the final revised version accepted for publication in Annali di Matematica Pura e Applicata Enrico Savi http://arxiv.org/abs/2603.15099v1 2026-03-16T10:50:45Z

An alternative proof of the completeness of relational algebra with respect to allowed formulas of first-order logic is presented. The proof relies on the well-known embedding of relational algebra into cylindric algebra, which makes it possible to establish completeness in a more algebraic way. Building on this proof, we present an alternative algorithm that produces a relational expression equivalent to a given allowed formula. The main motivation for the present work is to establish a proof of completeness suitable for generalisation to relational models handling incomplete or vague information.

2026-03-16T10:50:45Z Jan Laštovička http://arxiv.org/abs/2602.20380v2 2026-03-16T10:21:53Z

We show that the variety of modal lattices has the superamalgamation property. As a consequence, we obtain that the weak positive modal logic has the Craig interpolation property. Our proof employs the recent duality for modal lattices based on modal L-spaces. Moreover, we extend this result to a number of other weak positive modal logics axiomatized by modal axioms corresponding to universal Horn sentences.

2026-02-23T21:41:19Z Rodrigo Nicolau Almeida Nick Bezhanishvili Simon Lemal http://arxiv.org/abs/2603.14955v1 2026-03-16T08:10:05Z

In a recent work of Matteo Mio on compact quantitative equational theories (here compact means that all its consequences are derivable by means of finite proofs) convex algebras on the carrier set [0,1] whose operations are monotone and satisfy certain semicontinuity properties occurred. We fully classify those algebraic structures by giving an explicit construction of all possible convex operations on [0,1] possessing the mentioned properties. Our result thus describes exactly the range of theories to which Mio's theorem applies.

2026-03-16T08:10:05Z Ana Sokolova Harald Woracek http://arxiv.org/abs/2603.14924v1 2026-03-16T07:28:24Z

We give a proof of the o-minimal version of the Whitney Extension Theorem simplified as compared to the original ones. A new simplifying ingredient is a definable variant of Urysohn's lemma for class $\mathcal{C}^q$ (see Section 3).

2026-03-16T07:28:24Z 10 pages Beata Kocel-Cynk Wiesław Pawłucki Anna Valette http://arxiv.org/abs/2502.20751v2 2026-03-16T04:57:44Z

Hybrid logic extends modal logic with special propositions called nominals, each of which is true at only one state in a model. This enables us to describe some properties of binary relations, such as irreflexivity and anti-symmetry, which are essential to treat partial orders. We present terminating tableau calculi complete with respect to models whose accessibility relations are strictly partially ordered, unbounded strictly partially ordered, and partially ordered.

2025-02-28T06:00:49Z 29 pages, 8 figures Yuki Nishimura http://arxiv.org/abs/2509.19519v2 2026-03-15T17:35:01Z

We prove a theorem on iterated forcing that can be used for preservation of $\aleph_2$ and $\aleph_1$ in iterations with supports of size $\aleph_1$ of forcings that have amalgamation properties similar to those present in the perfect set forcing. The work is modelled after Baumgartner's Axiom A and his proof that iterations with countable support of the same preserve $\aleph_1$. In honour of James E. Baumgartner, the property introduced here is called Property B$(κ)$. The known additional difficulties when forcing at cardinals higher than $\aleph_1$ make for a less general theorem and a more complex theorem on the iteration, which is not an iteration theorem in the classical sense. The results extend to other cardinals $κ$ such that $κ^{<κ}=κ$, in place of $\aleph_1$. We give examples of individual forcings that have Property B$(κ)$ and their products. In particular, we introduce a correct version of the generalised perfect set forcing, which we call Perfect Set Forcing with Respect to a Filter. We give its basic properties and show that for the right kind of filter $\mathcal F$ this kind of forcing is iterable with supports of size $\leκ$.

2025-09-23T19:37:31Z A version after submission. We added an important comment at the beginning of S. 8, showing that we have to restrict our attention to certain kind of filters. In Ex. 8.1. we showing that such filters exist. We also added updates on the future directions and some references. We underlined the importance of Kanovei's 1999 result regarding the geometric iteration of the perfect set forcing Mirna Džamonja http://arxiv.org/abs/2603.14428v1 2026-03-15T15:11:16Z

This paper characterizes the covers of varieties of p-algebras in the lattice of quasivarieties of p-algebras. In particular, it is shown that every such variety has exactly one cover in the lattice of subquasivarieties. This answers a problem of Kowalski and Słomczyńska.

2026-03-15T15:11:16Z Zalán Gyenis http://arxiv.org/abs/2602.09143v3 2026-03-15T12:21:24Z

We investigate the following general problem, closely related to the problem of isomorphic classification of Banach spaces $C(K)$ of continuous real-valued functions on a compact space $K$, equipped with the supremum norm: Let $\mathcal{K}$ be a class of compact spaces. How many isomorphism types of Banach spaces $C(K)$ are there, for $K\in \mathcal{K}$? We prove that for any uncountable regular cardinal number $κ$, there exist exactly $2^κ$ isomorphism types of spaces $C(K)$ for compact spaces of weight $κ$. We show that, for the class $\mathcal{L}_{ω_1}$ of separable compact linearly ordered spaces of weight $ω_1$, the answer to the above question depends on additional set-theoretic axioms. In particular, assuming the continuum hypothesis, there are $2^{ω_1}$ isomorphism types of $C(L)$, for $L\in \mathcal{L_{ω_1}}$, and assuming a certain axiom proposed by Baumgartner, there is only one type.

2026-02-09T19:41:45Z Minor editorial improvements Maciej Korpalski Piotr Koszmider Witold Marciszewski http://arxiv.org/abs/2509.01830v3 2026-03-14T19:50:48Z

This article offers a gentle introduction to the axiom of choice. We introduce the axiom, discuss some common objections to it, and present three kinds of reasons to accept it. Although the exposition is aimed at non-experts in set theory, we also include some lesser-known results.

2025-09-01T23:19:27Z 12 pages Andreas Blass Dhruv Kulshreshtha