Issues

• Add a conjecture: smooth isometric embeddings of closed orientable surfaces in four-space

  new conjecture
  google-deepmind/formal-conjectures#7048 · Filter by author KitaKen1 opened on Oct 9, 2026

• Add a conjecture: infinitely many closed geodesic images on reversible Finsler spheres

  new conjecture
  google-deepmind/formal-conjectures#7041 · Filter by author KitaKen1 opened on Oct 9, 2026

• Agoh–Giuga: add the pointwise form of the equivalence

  google-deepmind/formal-conjectures#7040 · Filter by author still-rollin opened on Oct 9, 2026

• OEIS A060957: Lean-verified disproof of prime-exponent interpolation

  google-deepmind/formal-conjectures#7037 · Filter by author VictorLiwentao opened on Oct 9, 2026

• Add a conjecture: Tachikawa's second conjecture in characteristic zero

  new conjecture
  google-deepmind/formal-conjectures#7020 · Filter by author KitaKen1 opened on Oct 9, 2026

• Add a conjecture: mixed Fujita freeness and linear effective base-point freeness

  new conjecture
  google-deepmind/formal-conjectures#7012 · Filter by author KitaKen1 opened on Oct 9, 2026

• Add a conjecture: positive lower density of simultaneous primitive roots

  new conjecture
  google-deepmind/formal-conjectures#7011 · Filter by author KitaKen1 opened on Oct 9, 2026

• Erdős Problem 1133: status mismatch (repo=solved, erdosproblems.com=open)

  erdos-status-sync
  google-deepmind/formal-conjectures#7003 · Filter by author github-actions opened on Oct 8, 2026

• Add the Gaussian propeller partition bound

  google-deepmind/formal-conjectures#6997 · Filter by author anxkhn opened on Oct 8, 2026

• Add the separable quotient counterexample under CH

  google-deepmind/formal-conjectures#6996 · Filter by author anxkhn opened on Oct 8, 2026

• Add a quasinilpotent operator without a hyperinvariant subspace

  google-deepmind/formal-conjectures#6995 · Filter by author anxkhn opened on Oct 8, 2026

• Add bi-Lipschitz equivalent nonisomorphic separable Banach spaces

  google-deepmind/formal-conjectures#6994 · Filter by author anxkhn opened on Oct 8, 2026

• Add the doubling Hilbert dimension-reduction counterexample

  google-deepmind/formal-conjectures#6993 · Filter by author anxkhn opened on Oct 8, 2026

• Erdős 551: record the full cycle–clique Ramsey formula

  google-deepmind/formal-conjectures#6987 · Filter by author anxkhn opened on Oct 8, 2026

• Add asymptotically minimal maxima of real Littlewood polynomials

  google-deepmind/formal-conjectures#6986 · Filter by author anxkhn opened on Oct 8, 2026

• Add the Euclidean Steinitz–Bergström prefix bounds

  google-deepmind/formal-conjectures#6985 · Filter by author anxkhn opened on Oct 8, 2026

• Add nonexpansive fixed points in reflexive Banach spaces

  google-deepmind/formal-conjectures#6984 · Filter by author anxkhn opened on Oct 8, 2026

• Add Tingley's sphere-isometry extension theorem

  google-deepmind/formal-conjectures#6983 · Filter by author anxkhn opened on Oct 8, 2026

• Erdős Problem 348: status mismatch (repo=solved, erdosproblems.com=open)

  erdos-status-sync
  google-deepmind/formal-conjectures#6982 · Filter by author github-actions opened on Oct 8, 2026

• Add the linear list-Hadwiger bound

  google-deepmind/formal-conjectures#6976 · Filter by author anxkhn opened on Oct 8, 2026

• Add the Ramsey property for at most five points on a circle

  google-deepmind/formal-conjectures#6975 · Filter by author anxkhn opened on Oct 8, 2026

• Add the power-saving upper bound for planar halving lines

  google-deepmind/formal-conjectures#6974 · Filter by author anxkhn opened on Oct 8, 2026

• Add the origin-symmetric logarithmic Brunn–Minkowski inequality

  google-deepmind/formal-conjectures#6973 · Filter by author anxkhn opened on Oct 8, 2026

• Add the symmetric Mahler volume-product inequality

  google-deepmind/formal-conjectures#6972 · Filter by author anxkhn opened on Oct 8, 2026

• GreensOpenProblems/27: record the near-quadratic lower bound for m

  google-deepmind/formal-conjectures#6969 · Filter by author ashm1tr opened on Oct 8, 2026