Issues

• IsThreeManifoldWithBoundary is modelled on EuclideanHalfSpace 2, so it defines 2-manifolds with boundary

  facebookresearch/atlas-lean#602 · Filter by author Deicyde opened on Oct 30, 2026

• exists_twoAdic_oddPart_factorial_limit is false: the congruences at e = 2 and e = 3 are incompatible

  facebookresearch/atlas-lean#601 · Filter by author Deicyde opened on Oct 30, 2026

• not_dvd_lucasU_sum_of_gcd is false at n = 0 (missing 0 < n)

  facebookresearch/atlas-lean#600 · Filter by author Deicyde opened on Oct 30, 2026

• irwinSum_hasSum_alternating can be false at l = 1 (e.g. b = 10, d = 0, k = 0): the family is not absolutely summable, so HasSum fails

  facebookresearch/atlas-lean#599 · Filter by author Deicyde opened on Oct 30, 2026

• irwinMeasure_halfOpen_deeper_local_mass is false when 0 < d, l < l' and k = j

  facebookresearch/atlas-lean#598 · Filter by author Deicyde opened on Oct 30, 2026

• SkiRental: exists_cost_ge is trivially true with d = 0 and does not state the 2 - 1/B lower bound

  facebookresearch/atlas-lean#597 · Filter by author Deicyde opened on Oct 30, 2026

• DelannoyConstructionsWanted: genDelannoyLower_relations is false at n = k (fourth conjunct)

  facebookresearch/atlas-lean#596 · Filter by author Deicyde opened on Oct 30, 2026

• ScottishBook39Wanted: exists_discontinuous_subadditive_multiplicative is witnessed by the trivial φ (φ 0 = 0, φ x = 1 otherwise)

  facebookresearch/atlas-lean#595 · Filter by author Deicyde opened on Oct 30, 2026

• ScottishBook151Wanted: harmonicFunctionVanishesOnCubeEdges is trivial because U need not be connected

  facebookresearch/atlas-lean#594 · Filter by author Deicyde opened on Oct 30, 2026

• ScottishBook148Wanted: P ≠ 0 → A ↔ B parses as (P ≠ 0 → A) ↔ B, making the theorem_wanted false

  facebookresearch/atlas-lean#593 · Filter by author Deicyde opened on Oct 30, 2026

• MetaMathlibExt.lt_two_rpow_mul_mul_log_rpow is declared twice, so Autoform cannot link either copy to its article

  facebookresearch/atlas-lean#592 · Filter by author Deicyde opened on Oct 30, 2026

• ScottishBook117: HasTangentLineAt is an unoriented tangent, so cusps pass and Problem 117's claim is refuted trivially

  facebookresearch/atlas-lean#591 · Filter by author Deicyde opened on Oct 30, 2026

• ScottishBook69Wanted: ¬ ScottishBookProblem69Claim holds trivially via the empty space (no Nonempty E)

  facebookresearch/atlas-lean#590 · Filter by author Deicyde opened on Oct 30, 2026

• ScottishBook83Wanted: ¬ ScottishBookProblem83Claim holds trivially (f = id) because the Hölder conclusion is global on ℝ

  facebookresearch/atlas-lean#589 · Filter by author Deicyde opened on Oct 30, 2026

• ContDiff ℝ ⊤ means analytic, not C^∞, in ScottishBook17Point1Wanted and ParametricSard

  facebookresearch/atlas-lean#588 · Filter by author Deicyde opened on Oct 30, 2026

• HybridPrimeDivisorBoundsWanted: four bounds are nearly vacuous for even n, because Nat.nth returns 0 past the end of a finite prime class

  facebookresearch/atlas-lean#587 · Filter by author Deicyde opened on Oct 30, 2026

• ScottishBook169: IsCountablyAdditive puts the implication inside the Pairwise lambda, forcing μ into {0, ∞}

  facebookresearch/atlas-lean#586 · Filter by author Deicyde opened on Oct 30, 2026

• Merge queue: v1 FourierAnalysis and ComplexVariables ports (Deicyde fork)

  facebookresearch/atlas-lean#407 · Filter by author Deicyde opened on Oct 25, 2026

• Record and verify the Formal-Math → ATLAS v2 sync boundary

  facebookresearch/atlas-lean#157 · Filter by author Deicyde opened on Oct 14, 2026
  1

• Publish a verified Autoform library index for ATLAS v2

  facebookresearch/atlas-lean#156 · Filter by author Deicyde opened on Oct 14, 2026
  3

• natDegree_realCyclotomicPolynomial is declared in two MathlibExt modules

  facebookresearch/atlas-lean#148 · Filter by author zibo-yang opened on Oct 11, 2026