Wikipedia/IdonealCompleteness: prove knownIdonealNumbers_are_idoneal

[williamjblair]

Proves knownIdonealNumbers_are_idoneal — all 65 known idoneal numbers are in fact idoneal.

The work is making the predicate decidable. IsIdoneal n is 0 < n ∧ ¬ ∃ a b c, 0 < a < b < c ∧ n = a*b + b*c + a*c, and that existential ranges over unbounded ℕ. The helper exists_triple_iff_bounded reduces it to a bounded double-search: for a fixed pair a, b ≤ n the constraint pins c = (n − a*b)/(a+b) exactly, so only a, b are searched (over Finset.range (n+1)), with a, b ≤ n falling out of nlinarith on 0 < a < b < c. The main proof then fin_cases over the 65 numbers, peels off the trivial 0 < n, and discharges each bounded search.

This one needs native_decide: plain decide is infeasible — the kernel's Finset reduction hits maxRecDepth on a bounded search as small as 100×100, long before the n = 1848 cases. So #print axioms includes Lean.ofReduceBool (the compiler-checked-computation axiom) alongside the usual [propext, Classical.choice, Quot.sound]; no sorryAx. The file builds in ~13s.

Only knownIdonealNumbers_are_idoneal is touched; the research-open idoneal_numbers_completeness keeps its sorry.

Drafted with AI assistance and machine-checked by the Lean kernel.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[mo271]

Thanks, LGTM