From b724ac5bbb6444c7646612c0939a9efab553d9c2 Mon Sep 17 00:00:00 2001
From: Kenny Lau <kc_kennylau@yahoo.com.hk>
Date: Fri, 11 Sep 2026 10:49:48 +0000
Subject: [PATCH] feat: add formalization.yaml

---
 formalization.yaml | 85 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 85 insertions(+)
 create mode 100644 formalization.yaml

diff --git a/formalization.yaml b/formalization.yaml
new file mode 100644
index 0000000..81a2c2a
--- /dev/null
+++ b/formalization.yaml
@@ -0,0 +1,85 @@
+# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json
+
+version: "v0.4"
+
+project:
+  name: "TanArctan"
+  authors: [Kenny Lau]
+  description: >
+    `TanArctan` is a formal proof of the divisibility barrier and the bound on the exceptional set
+    in *Integer values of $\tan(\arctan 1+\arctan 2+\cdots+\arctan n)$ are rare*
+    (arXiv:2607.05739). It proves Theorem 1.1, the proximity estimate (12) in the proof of
+    Lemma 3.1, and Lemma 3.1 itself. The Lean files were generated by AxiomProver, Axiom Math's
+    in-house theorem proving system.
+  responsible_maintainers: [Kenny Lau]
+  license: "MIT"
+
+repository:
+  role: "substantive-development"
+
+sources:
+  - title: "Integer values of $\\tan(\\arctan 1+\\arctan 2+\\cdots+\\arctan n)$ are rare"
+    authors: [Ken Ono]
+    id: "https://arxiv.org/abs/2607.05739"
+    type: "article"
+    location: "Theorem 1.1, equation (12), Lemma 3.1"
+    relationship: "formalizes"
+    note: >
+      Formalizes the two barriers an integer value must clear and the logarithmic bound on the
+      indices where they do not yet bite.
+
+classification:
+  arxiv: [math.NT, math.CO]
+  msc2020: [11D09, 11N37]
+
+status:
+  scope: >
+    Theorem 1.1 for every $n \ge 1$ with $A_n \ne 0$, equation (12) for every $n \in E$, and
+    Lemma 3.1. `problem.lean` defines $E$ as $\{n \ge 5 : A_n = 0 \text{ or } |x_n| > n/2 + 1\}$,
+    so an index where $x_n$ is undefined counts as exceptional.
+  sorry_count: 0
+  sorry_in_definitions: 0
+  axioms: [propext, Quot.sound, Classical.choice]
+  main_results:
+  - declaration: "thm_main"
+    file: "output/solution.lean"
+    sorry_count: 0
+    axioms: [propext, Quot.sound, Classical.choice]
+    comparator_config: "comparator.json"
+  - declaration: "lem_proximity"
+    file: "output/solution.lean"
+    sorry_count: 0
+    axioms: [propext, Quot.sound, Classical.choice]
+    comparator_config: "comparator.json"
+  - declaration: "cor_density"
+    file: "output/solution.lean"
+    sorry_count: 0
+    axioms: [propext, Quot.sound, Classical.choice]
+    comparator_config: "comparator.json"
+
+automation:
+  methods:
+    - method: "autonomous"
+      models: [AxiomProver]
+
+review:
+  status: "author-verified"
+  reviewers: [Kenny Lau]
+  notes: >
+    The formal challenge in `output/problem.lean` was checked against the source paper by an
+    author of that paper.
+
+alignment:
+  statements:
+    - source: "Integer values of $\\tan(\\arctan 1+\\arctan 2+\\cdots+\\arctan n)$ are rare (Theorem 1.1 (1), and the first assertion of (2))"
+      lean: "thm_main"
+      module: "output.solution"
+      status: "Proved."
+    - source: "Integer values of $\\tan(\\arctan 1+\\arctan 2+\\cdots+\\arctan n)$ are rare (equation (12), in the proof of Lemma 3.1)"
+      lean: "lem_proximity"
+      module: "output.solution"
+      status: "Proved, with the distance to $\\tfrac{\\pi}{2}\\mathbb{Z}$ given by an explicit integer $j$."
+    - source: "Integer values of $\\tan(\\arctan 1+\\arctan 2+\\cdots+\\arctan n)$ are rare (Lemma 3.1)"
+      lean: "cor_density"
+      module: "output.solution"
+      status: "Proved, with $O(\\log N)$ written out as explicit constants $C$ and $N_0$."