Papers With

← All papers
First page of Construction and formal verification of a special topology on {\mathbb{Z}}^{n}: characterization of connected subsets

Construction and formal verification of a special topology on {\mathbb{Z}}^{n}: characterization of connected subsets

Ignacio Vega-Páez

cs.SC Oct 29, 2026 · v1 cs.LO
formalization mathlib topology
Read PDF arXiv abstract
TL;DR
Formalizes in Lean 4 with Mathlib the Marcus–Wyse topology on Z^n and the equivalence between connectedness (IsPreconnected) and lattice-path accessibility.
Abstract
We examine whether the integers admit a topology whose connected subsets are precisely the sets of consecutive integers. The main result gives a construction for every integer lattice {\mathbb{Z}}^{n}, n>0; the answer for Z is then obtained as a corollary. We prove that the neighborhoods determined by the parity of the sum of the coordinates form a basis and that topological connectedness agrees exactly with accessibility by finite paths of unit lattice steps. We also present a deductive audit and the correspondence between this argument and a verification in Lean 4 and Mathlib, including the empty set and the independent formal characterization of integer intervals. The construction and mathematical result originate in Problem 5712, proposed by Dan Marcus and solved in 1970 by the Cleveland State University group; the present article contributes a detailed exposition and a report on formal verification.
Problem

Problem 5712 of the American Mathematical Monthly asks whether the integers carry a topology whose connected subsets are exactly the sets of consecutive integers. The question generalizes to Z^n, where consecutiveness becomes accessibility by finite paths of unit lattice steps.

Approach

A basis is defined on Z^n by parity of the coordinate sum: points with an even sum get the point plus its unit neighbors as a neighborhood, and points with an odd sum get a singleton. The proof shows this is a basis and that subspace connectedness is equivalent to path accessibility, and derives the integer case as a corollary. The argument is verified in Lean 4/Mathlib, with Z^n represented as Fin n → ℤ and paths encoded through Relation.EqvGen and ReflTransGen. IsPreconnected is used instead of IsConnected so that the empty set is handled correctly.

Results

The general theorem for Z^n and the integer-interval corollary, including the formulas for the basic neighborhoods, compile in Lean 4.36.0-rc1 with Mathlib. The build has no errors, sorry, or new axioms.