SearcharxivSearch

arXiv subjects

Benedikt Stock

Publications and source records attributed to Benedikt Stock.

5 recordsLinked to original sources

The Galois characterisation of $p$-adically closed fields -- A modern perspective

In 1927, Artin and Schreier showed that a field is real closed if and only if its absolute Galois group has order two. Inspired by this characterisation and drawing on earlier work of Neukirch, Pop conjectured the following $p$-adic analogue: a field is $p$-adically closed if and only if its absolute Galois group is isomorphic to that of $\mathbb{Q}_p$. In 1995, the conjecture was independently solved by Efrat for $p \ne 2$ and by Koenigsmann in full generality. Using novel techniques in the theory of valued fields developed over the last 25 years, we give a new, elementary, and self-contained proof of this theorem, with a Galois characterisation of henselianity at the heart of the proof and without relying on Galois cohomology. We further highlight connections to the recent work of Jahnke-Kartas on perfectoid fields and model-theoretic transfer techniques. We provide a systematic account of all of our methods to encourage further investigations.

math.NT

Unsupervised Learning of Invariance Transformations

The need for large amounts of training data in modern machine learning is one of the biggest challenges of the field. Compared to the brain, current artificial algorithms are much less capable of learning invariance transformations and employing them to extrapolate knowledge from small sample sets. It has recently been proposed that the brain might encode perceptual invariances as approximate graph symmetries in the network of synaptic connections. Such symmetries may arise naturally through a biologically plausible process of unsupervised Hebbian learning. In the present paper, we illustrate this proposal on numerical examples, showing that invariance transformations can indeed be recovered from the structure of recurrent synaptic connections which form within a layer of feature detector neurons via a simple Hebbian learning rule. In order to numerically recover the invariance transformations from the resulting recurrent network, we develop a general algorithmic framework for finding approximate graph automorphisms. We discuss how this framework can be used to find approximate automorphisms in weighted graphs in general.

cs.NE

Mathematical Proof Between Generations

A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time this has been a topic for experts in specialized communities. However, mathematical proofs have become increasingly sophisticated, stretching the boundaries of what is humanly comprehensible, so that leading mathematicians have asked for formal verification of their proofs. At the same time, major theorems in mathematics have recently been computer-verified by people from outside of these communities, even by beginning students. This article investigates the gap between the different definitions of a proof and possibilities to build bridges. It is written as a polemic or a collage by different members of the communities in mathematics and computer science at different stages of their careers, challenging well-known preconceptions and exploring new perspectives.

math.HO

An elementary proof of the local Kronecker-Weber theorem

We will present a novel elementary, self-contained, and explicit proof of the local Kronecker-Weber theorem. Apart from discrete valuation theory, it does not make use of any tools beyond those introduced in a second undergraduate course on algebra. In particular, we will not make use of results from local class field theory or Galois cohomology.

math.NT

Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle

How difficult are interactive theorem provers to use? We respond by reviewing the formalization of Hilbert's tenth problem in Isabelle/HOL carried out by an undergraduate research group at Jacobs University Bremen. We argue that, as demonstrated by our example, proof assistants are feasible for beginners to formalize mathematics. With the aim to make the field more accessible, we also survey hurdles that arise when learning an interactive theorem prover. Broadly, we advocate for an increased adoption of interactive theorem provers in mathematical research and curricula.

cs.LO