Main conjecture on fusible numbers
Main conjecture on fusible numbers
Inferred from the community field; finer classification has not been reviewed.
Problem statement
conj_7_1
If x is a fusible number and y is its successor, then the interval [x + 1, y + 1) can be
divided into intervals [ℓₙ, ℓₙ₊₁), such that the fusible numbers in [ℓₙ, ℓₙ₊₁) are obtained by
fusing the n + 1st successor of x with a fusible number.
This formalization differs from Conjecture 7.1 in the paper in four ways:
(1) it is obtained from Conjecture 7.1 by plugging in n + 1 into n, which simplifies the expressions
and removes the need to assume n ≥ 1;
(2) the n + 1st successor s^(n+1)(x) is replaced by the explicit value x + (2 - 1 / 2 ^ n) * m;
(3) instead of defining y to be the successor of x, we assert that there is no fusible number
strictly between x and y;
(4) instead of using ∃ z, IsFusible z ∧ q = s^(n+1)(x) ~ z we use the value of z determined by the equality,
namely z = 2 * q - 1 - s^(n+1)(x), and it is easy to see z ∈ [x + 1 - m / 2 ^ n, x + 1) as required.
Lean 4
Formal statement
Lean 4/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtil
/-!
# Main conjecture on fusible numbers
*References:*
- [Fusible numbers and Peano Arithmetic](https://arxiv.org/abs/2003.14342),
by Jeff Erickson, Gabriel Nivasch, and Junyan Xu.
- [Fusible numbers and Peano Arithmetic](https://doi.org/10.46298/lmcs-18%283%3A6%292022),
Logical Methods in Computer Science, Volume 18, Issue 3 (July 28, 2022).
-/
namespace FusibleNumber
/--
A rational number is fusible if it belongs to the smallest set containing $0$ and closed under
the operation
$$
a \sim b = \frac{a + b + 1}{2}
$$
whenever $|a-b| < 1$.
-/
inductive IsFusible : ℚ → Prop
| zero : IsFusible 0
| fuse (a b : ℚ) : IsFusible a → IsFusible b → |a - b| < 1 → IsFusible ((a + b + 1) / 2)
/-- The rational number $1/2$ is fusible. -/
@[category test, AMS 5]
theorem isFusible_one_half : IsFusible (1 / 2 : ℚ) := by
have h := IsFusible.fuse 0 0 IsFusible.zero IsFusible.zero (by norm_num)
norm_num at h
exact h
/-- The rational number $1$ is fusible. -/
@[category test, AMS 5]
theorem isFusible_one : IsFusible (1 : ℚ) := by
have h := IsFusible.fuse (1 / 2) (1 / 2) isFusible_one_half isFusible_one_half (by norm_num)
norm_num at h
exact h
/-- If `x` is a fusible number and `y` is its successor, then the interval `[x + 1, y + 1)` can be
divided into intervals `[ℓₙ, ℓₙ₊₁)`, such that the fusible numbers in `[ℓₙ, ℓₙ₊₁)` are obtained by
fusing the `n + 1`st successor of `x` with a fusible number.
This formalization differs from Conjecture 7.1 in the paper in four ways:
(1) it is obtained from Conjecture 7.1 by plugging in `n + 1` into `n`, which simplifies the expressions
and removes the need to assume `n ≥ 1`;
(2) the `n + 1`st successor `s^(n+1)(x)` is replaced by the explicit value `x + (2 - 1 / 2 ^ n) * m`;
(3) instead of defining `y` to be the successor of `x`, we assert that there is no fusible number
strictly between `x` and `y`;
(4) instead of using `∃ z, IsFusible z ∧ q = s^(n+1)(x) ~ z` we use the value of `z` determined by the equality,
namely `z = 2 * q - 1 - s^(n+1)(x)`, and it is easy to see `z ∈ [x + 1 - m / 2 ^ n, x + 1)` as required. -/
@[category research open, AMS 5]
theorem conj_7_1 (x y q : ℚ) (n : ℕ) (fus_x : IsFusible x) (fus_y : IsFusible y) (lt : x < y)
(nmem_Ioo : ∀ z, IsFusible z → z ∉ Set.Ioo x y) :
let m := y - x
let ℓ (n : ℕ) := y + 1 - m / 2 ^ n
IsFusible q → q ∈ Set.Ico (ℓ n) (ℓ (n + 1)) → IsFusible (2 * q - 1 - x - (2 - 1 / 2 ^ n) * m) := by
sorry
end FusibleNumber
On-site verification needs an executable Lean target. None is attached yet.
A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.
Proofs & verification
No Lean has been submitted for this problem yet. A Lean file can be attached to a submission for review, though with no target here it cannot be machine-checked.
Background
Source snapshot inspected on 10 September 2026. Subsequent research status and the accuracy of source formalizations have not been independently certified.
Fixed commit b82b08faa9006484021c12005ab41287fb2ffb69. This file contains 1 source-labeled research-open declarations. Other declarations in the attached file can be definitions, solved results or tests. The file is preserved as source material; it has not been compiled or proved by this import.
Copyright The Formal Conjectures Authors. Code: Apache-2.0; other original material: CC BY 4.0. Third-party sources retain their own licenses. Original source files and notices preserved.
Recorded progress
Add yours →Nothing recorded yet. A pointer to a paper the entry is missing counts.
Machine attempts
0 recordedAttempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.
No machine attempts recorded.
Sign in to run an attempt. New accounts start with enough credits for ten.
Discussion
0 notesNotes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.
No notes yet.
Sign in to add a note.