{"id":"ea2f35ec-3f6d-4dd6-ac98-2e660e056dc3","arxiv_id":"2608.06682","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For intervals of length H = X^{1/5 - 2/90935 + ε}, the number of squarefree integers differs from (6/π²)H by at most an explicit constant times H X^{-ε/10^{25}}.","lead":"A number theory note makes explicit the author's earlier result on squarefree numbers in short intervals, with a fully explicit error term and a machine-checked Lean 4 proof in a GitHub repository. The theorem gives a power-saving estimate that is now checkable by a computer, showing a path toward formalized analytic number theory.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The theorem depends on an unproved, non-explicit Proposition 3.1; Remark 1 concedes the printed version is a weakened proxy for the formalized bound actually used.","rationale":"The reader correctly identifies Proposition 3.1 as the load-bearing assumption, and I agree that the absence of a derivation is a serious gap. My stress-test sharpens the concern: the issue is not only that Proposition 3.1 is unproved, but that the printed proposition is not sufficient for Theorem 1.1. It is asymptotic, with an unspecified U^{O(1)} exponent and no explicit constants, while the theorem claims an explicit numerical bound. More importantly, Remark 1 says the proposition is a weakened version of the formalized result: the Lean proof bounds N_a(H,D), a finer quantity whose range depends on a as well as Δ. Consequently, even a mathematically correct proof of the printed Proposition 3.1 would not establish the printed Theorem 1.1 without additional, unstated work. The paper does not display the explicit version used, so the text alone is internally incomplete. I do not reject the work, because a genuine Lean 4 formalization would be strong evidence and could close the gap; but the preprint as written cannot be fully verified. The reader's CONDITIONAL verdict is therefore appropriate, with the condition being: supply the pinned repository and verification transcript, or reproduce the explicit Proposition 3.1 and its proof in the text. My agreement is only partial because I locate the problem more strongly: the printed proposition is not merely missing its proof, it is missing the precision and content needed for the theorem.","tokens_in":3739,"tokens_out":4408,"duration_ms":46040,"concrete_test":"Pin the linked GitHub repository to an exact commit, run `lake build` under Lean 4, and confirm that no `axiom`, `sorry`, or `admit` appears in the dependency closure of `count_short_interval_eps` at squarefree_lean/Squarefree/ExplicitBounds.lean:765. Then verify that the statement of that theorem matches (1) with the explicit constant 10^450 and exponent epsilon/10^25, and that its proof depends on Squarefree.dblock_on_strip_explicit with the full derivation of the explicit version of Proposition 3.1. If the build succeeds and the statement matches, the missing proof is supplied by the formalization; if not, Theorem 1.1 is unverified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central result rests on the critical-range bound for N(H,D), stated as Proposition 3.1. As printed, that proposition cannot by itself support Theorem 1.1. First, it is asymptotic: N(H,D) is bounded by H times (1/U + U^{O(1)}(...)), with an unspecified O(1) in the exponent and an implied constant that is not given. An explicit theorem with constants like 10^450 cannot be read off from such a statement. Second, no proof is supplied; the text refers to the Lean repository instead of deriving the bound from the differencing identity (9). Third, Remark 1 explicitly says the proposition is a weakening of what is actually formalized: the formalization bounds N_a(H,D), and the relevant ranges depend on a as well as on Δ. Thus the printed lemmas are not the lemmas used, and the theorem in Lean is stronger than what the note states. If the explicit version of Proposition 3.1 has an error—for example, a miscounted carry shift ρ_i in (9) or a gap at the transition between the ranges of Proposition 2.3 and the critical range—the bound in Theorem 1.1 would fail. The text gives no way to check this without the repository, and the repository is not pinned to a commit.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript announces an explicit, Lean-formalized power-saving estimate for the number of squarefree numbers in short intervals. Theorem 1.1 states that, for 0 < ε ≤ 1/90935, X ≥ exp(10^27/ε^2), and H = X^{1/5 - 2/90935 + ε}, the deviation of the squarefree count in [X, X+H] from (6/π^2)H is at most (10^450/ε) H X^{-ε/10^25}. The argument follows the author's earlier work [Pan24], replacing the Green-Tao nilsequence input in the critical range by elementary van der Corput differencing on a bracket expression, and states the necessary critical-range bound as Proposition 3.1. The paper explicitly acknowledges in Remark 1 that the printed propositions are weakened versions of the statements actually formalized in the linked Lean repository.","tokens_in":3978,"tokens_out":3542,"duration_ms":34909,"significance":"If the formalized proof is correct, this is a substantial result: it gives the first fully explicit, machine-checked power saving for squarefree numbers in short intervals, with a printed constant of order 10^450. The decision to avoid Fourier analysis by using elementary Swinnerton-Dyer bounds is a useful simplification that may make the argument easier to formalize and verify. The existence of a machine-checked proof is a genuine strength, but it is only accessible if the repository is pinned and fully inspectable. As submitted, the manuscript does not provide enough information to verify the central claim from the printed text alone, which substantially limits the significance of the announcement.","major_comments":[{"comment":"Proposition 3.1 is the critical-range input for Theorem 1.1, but as printed it cannot support the theorem. It asserts N(H,D) ≪ H (1/U + U^{O(1)}(...)) with an unspecified constant in the O(1) exponent and an implied constant in the ≪ notation. Since Theorem 1.1 is an explicit bound with constants such as 10^450 and exponent -ε/10^25, the reader cannot pass from (10) to (1). The text also gives no proof of Proposition 3.1: it only cites Lean identifiers. In particular, the derivation from the differencing identity (9) is not shown, including how the union bound over the integer carry shifts ρ_i yields the displayed exponents in (10). I request that the explicit form of Proposition 3.1 with all constants be stated and proved in the text or in an appendix.","section":"§3, Proposition 3.1"},{"comment":"Remark 1 concedes that the printed statements are weakened proxies for the formalized results. Specifically, the formalized object is N_a(H,D), and the applicability of Squarefree.prop_5_1 versus Squarefree.prop_7_3 depends on the scale of a as well as on Δ. The manuscript does not state the explicit bound for N_a(H,D) that is actually proved, nor does it explain how Theorem 1.1 follows from bounds on N_a rather than on N(H,D). This leaves a gap in the logical chain from the displayed propositions to the theorem.","section":"Remark 1"},{"comment":"The preparatory propositions are also asymptotic statements with omitted constants and, in Proposition 3.1, an unspecified U^{O(1)}. Proposition 2.2 gives C=10^20 but later uses require a precise relation among U, Δ, G, H, and ε. The manuscript does not show the optimization step that selects U and Δ so that the combination of Propositions 2.3 and 3.1 yields a bound of the form H X^{-ε/10^25}. Without this calculation, the claimed numerical value 10^450 in Theorem 1.1 cannot be checked from the text.","section":"§2, Propositions 2.1–2.3"}],"minor_comments":[{"comment":"The title as printed contains typographical spacing errors: 'SHOR T INTER V ALS' should be 'SHORT INTERVALS'.","section":"Title"},{"comment":"The GitHub repository is referenced by URL but is not pinned to a commit, and no build instructions or specific Lean version are given. For a formalization to be verifiable, the exact commit and environment are needed.","section":"Repository information"},{"comment":"The summation notation in (9) is difficult to parse: '3X i≤3 j<ks.t.{1,2,3}={i,j,k}' appears to be a mangled summation; please use standard sum notation with explicit index sets.","section":"Equation (9)"},{"comment":"The sentence 'This role was played in the original paper by [Pan24, Proposition 2.2], which is a bit stronger then 2.1' contains a typo: 'then' should be 'than'.","section":"Page 2"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First, the actual news: Pandey gets an explicit power-saving bound for squarefree numbers in short intervals by replacing the non-explicit Green–Tao input with elementary van der Corput differencing, and he claims a Lean 4 formalization of the whole thing. The exponent 2/90935 and the enormous X lower bound are far from practical, but that is not the point. An explicit, machine-checked theorem of this classical type is a genuine milestone, and the candid account of AI-assisted formalization is useful for people thinking about how to do serious verification work. The paper is honest about what is formalized and does not oversell the mathematics.\n\nThe soft spots are real, though they are mostly about verifiability, not about the mathematical spine. Proposition 3.1, the critical-range bound, is stated only asymptotically, with an e, a U^O(1), and unspecified implied constants. The text alone cannot produce the 10^450 constants in Theorem 1.1. Remark 1 explicitly concedes that the printed proposition is a weakening of what is actually proved in Lean: the formalized result bounds N_a(H,D) and the relevant ranges depend on a. So the printed lemmas do not fully match the proof, and the repository is not pinned to a commit, with no build or verification instructions. A reader who cannot or will not dig through the Lean code has no way to check the key step. That is a serious accessibility gap for a paper whose main claim to verification is the formalization.\n\nI do not think the paper is circular or fudging. The argument is conditional on the correctness of the formalization, and the authors are explicit about the gap between the note and the code. The differencing identity (9) and the union-bound over carry shifts are plausible and consistent with the earlier framework. There is no fitting or definitional sleight of hand here. So the central claim is not obviously wrong; it is simply unverifiable from the PDF.\n\nFor peer review, this should be engaged with, not desk-rejected. A serious referee could check the repository, pin the commit, and run the Lean code. The journal should require that the repo be pinned and that either Proposition 3.1 be stated explicitly in its true formalized form or the full proof be made available in a documented supplementary file. Without those, the printed note is not self-contained. I would cite this only after the repo is pinned and verified, not before. Reading group: maybe, as a data point about automated formalization, but not for the number theory itself.","headline":"The formalization is the real claim and the real risk; the printed note cannot carry the theorem alone, but the approach is honest and deserves a serious referee.","tokens_in":4494,"tokens_out":2511,"would_cite":false,"duration_ms":27038,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["11N25","11N37","11L07"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper makes explicit and machine-checks a power-saving error bound for squarefree numbers in short intervals: for admissible ε and enormous X, with H = X^(1/5 − 2/90935 + ε), the squarefree count in [X, X+H] is within (10^450/ε) H…","keywords":["squarefree numbers","short intervals","explicit estimates","van der Corput differencing","bracket polynomials","formal verification","power-saving error"],"falsifier":"Since the stated $X$ is astronomically large, a direct numerical search cannot reach the theorem's range; the concrete check is to verify Proposition 3.1's bound for $N(H,D)$ on the critical scale, for example by taking a small but admissible $X$ and admissible $\\varepsilon$, choosing $D$ in the critical range (7), and searching for $d \\in [D,2D]$ with $\\|X/d^2\\| \\le H/D^2$. A single $d$ exceeding the claimed bound would invalidate the key step, as would a flaw found in the formal derivation of Proposition 3.1.","tokens_in":3534,"feed_emoji":"🔢","tokens_out":8560,"duration_ms":78967,"temperature":0.7,"pith_summary":"The paper gives a fully explicit version of the author's earlier result on squarefree numbers in short intervals: for any $0 < \\varepsilon \\le 1/90935$ and $X \\ge \\exp(10^{27}/\\varepsilon^2)$, with $H = X^{1/5 - 2/90935 + \\varepsilon}$, the number of squarefree integers in $[X, X+H]$ is within $(10^{450}/\\varepsilon)\\,H\\,X^{-\\varepsilon/10^{25}}$ of the expected value $(6/\\pi^2)H$. The interest is that both the exponent and every constant are pinned down, and the proof is recorded in a machine-checked formalization. The note explains the main new step: the previously nonexplicit range, which came from quantitative equidistribution of nilsequences, is handled here by elementary van der Corput differencing applied to a bracket expression, together with a union bound over finitely many integer carry shifts. If correct, this removes the last ineffective ingredient from the estimate.","feed_headline":"Squarefree count error made explicit and machine-checked","feed_subtitle":"Every constant pinned down: the count deviates from (6/pi^2)H by a power-saving error.","key_machinery":"The central object is $N(H,D)$, the count of $d\\in[D,2D]$ for which the fractional part of $X/d^2$ lands within $H/D^2$ of an integer. The argument bounds $N(H,D)$ by splitting into ranges and applying three propositions; the crucial new tool is the explicit finite-difference identity (9) for the bracket expression $g(r)$, which lets the author reduce nonconcentration of $g$ to a union bound over $O(1)$ integer carry shifts $\\rho_0,\\ldots,\\rho_3$. Combined with van der Corput differencing and an elementary estimate for lattice points on a convex curve, this gives Proposition 3.1, the critical-range estimate that makes the exponent explicit.","core_discovery":"Theorem 1.1 states that the deviation of the squarefree count in an interval of length $H$ from the expected $(6/\\pi^2)H$ is at most an explicit power-saving multiple of $H X^{-\\varepsilon/10^{25}}$. The proof reduces the count to bounding $N(H,D) = \\#\\{d\\in[D,2D] : \\|X/d^2\\| \\le H/D^2\\}$ across all relevant scales of $D$. Three propositions cover the easy ranges, and the critical range, previously handled by a nonexplicit equidistribution theorem, is covered by Proposition 3.1, an upper bound obtained by finite differencing of the bracket expression $g(r) = f_3(r) + f_1(r)\\{f_2(r)\\}$. The finite-difference identity (9) shows that after differencing three times, the bracket expression reduces to a sum of monomials plus a small error, with the carry information encoded in finitely many bounded integers; the paper splits over those possibilities by a union bound instead of proving equidistribution. The assembled result is an explicit bound for $N(H,D)$ in the critical range, which yields Theorem 1.1.","pith_inferences":["The union-bound over integer carry shifts in identity (9) is a general recipe: any problem where a nilsequence reduces to a bracket polynomial with integer-valued floors could be made explicit in the same way, without a full equidistribution theorem.","Because Proposition 3.1 is the only unproved ingredient in the expository text, the formal proof files, not the note itself, are the real authority for the critical step; a reader who cannot inspect them must take that proposition on faith.","The exponent $2/90935$ is not likely to be optimal; the author explicitly trades some sharpness for simplicity of exposition, so tightening the choices in Proposition 3.1 would plausibly yield a larger power saving.","The explicit nature of the bound invites a computational check on intermediate scales: even though the full $X$ range is out of reach, the inequality for $N(H,D)$ in the critical scale could be tested numerically to probe whether the shape of Proposition 3.1 is plausible."],"forward_implications":["If Theorem 1.1 is correct, the error term $H X^{-\\varepsilon/10^{25}}$ gives a fully explicit power saving for every admissible $\\varepsilon$, not just an asymptotic one.","Every constant in the estimate is computable, so the bound can be used as a black box in other arguments without worrying about ineffective constants.","The critical range no longer depends on a nonexplicit equidistribution theorem; the proof uses only elementary differencing and a union bound over carry shifts.","The machine-checked formalization means the statement of Theorem 1.1 has been verified mechanically, assuming the correctness of the formal proof system itself.","The explicit exponent $1/5 - 2/90935$ is the bottleneck produced by Proposition 3.1; any improvement in that proposition would directly improve the exponent in the theorem."],"supporting_citations":[{"why":"Supplies the original result on squarefree numbers in short intervals, the reduction to counting $N(H,D)$, and the setup that the present paper makes explicit.","marker":"[Pan24]"},{"why":"Provides the quantitative equidistribution theorem for polynomial orbits on nilmanifolds that previously made the exponent nonexplicit; the present paper avoids using it.","marker":"[GT12]"},{"why":"Supplies the elementary bound for lattice points on convex curves that the formalization uses in place of Fourier analysis in Proposition 2.2.","marker":"[SD74]"}],"fun_headline_variants":["Explicit error bound for squarefree counts, formalized in Lean","Machine-checked proof of squarefree interval error","Explicit squarefree count error via finite differencing","Formalized explicit bound for squarefree density error","Squarefree interval error: fully explicit and Lean-verified"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole explicit bound depends on Proposition 3.1, a bound for the critical range that the note states without proof and leaves to the accompanying formal proof files; if that proposition is wrong, Theorem 1.1 collapses.","fun_headline_variants_meta":{"raw":{"variants":["Explicit error bound for squarefree counts, formalized in Lean","Machine-checked proof of squarefree interval error","Explicit squarefree count error via finite differencing","Formalized explicit bound for squarefree density error","Squarefree interval error: fully explicit and Lean-verified"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000172,"raw_usage":{"total_tokens":1270,"prompt_tokens":934,"completion_tokens":336,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":550,"completion_tokens_details":{"reasoning_tokens":271}},"tokens_in":550,"tokens_out":336,"duration_ms":3317,"temperature":1.0,"reasoning_tokens":271,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T22:31:57.898053+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Since the stated $X$ is astronomically large, a direct numerical search cannot reach the theorem's range; the concrete check is to verify Proposition 3.1's bound for $N(H,D)$ on the critical scale, for example by taking a small but admissible $X$ and admissible $\\varepsilon$, choosing $D$ in the critical range (7), and searching for $d \\in [D,2D]$ with $\\|X/d^2\\| \\le H/D^2$. A single $d$ exceeding the claimed bound would invalidate the key step, as would a flaw found in the formal derivation of Proposition 3.1.","supporting_citations":[],"review_version":1}