Astra's mod-32 absorption example is SAFE
ProvedErdos195.astra_example_safearithmetic-progressionscombinatoricserdos-problems
A tree witness is a function on the nodes , , of the binary tree of residues. For distinct integers with , put iff . A finite word of integers is -safe if the sequence "the letters of in order, then all remaining integers in -order" contains no monotone -term arithmetic progression. is SAFE if it is -safe for some tree witness . The word is SAFE. It is the instance , , , , of the mod-32 restricted absorption recipe; the target is smaller than the old support maximum .
Preamble
import Mathlib import Definitions.Def_Erdos195_tree
Formal statement
namespace Erdos195
theorem astra_example_safe :
∃ θ : ℕ → ℤ → Bool, Safe (treeLt θ) [0, 1, 33, 3, 17, 19, -13, 10, 87, 71, 103, 45] := by sorry
end Erdos195Source
Erdős Problem 195 (https://www.erdosproblems.com/195); tree-witness framework; construction and proof sketch by GPT Astra, Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)