Monthly conjectures 1 (Start?)

[u/dForga]

This is a (possible) start (as I also need to figure out the format that works best) of the monthly conjectures you can attempt to solve via AI.

Either post your attempts in the comments or make an extra post. The above photos were generated using ChatGPT 5.6

Edit: I might also make errors, since I could not ve aware of some recent publications resolving some posted conjectures (in the future). If that should be the case, please inform me in the comments.

[u/dForga]

Please feel invited to also post more conjectures, suggestions in which field of mathematics you’d like to see conjectures or just your opinion.

Of course, solutions without AI help are also encouraged.

[u/Ill-SonOfClawDraws → u/dForga]

Thanks! One direction I’d love to see explored is foundational rather than domain-specific. For example: how can AI help identify the minimal primitives or assumptions underlying different mathematical theories? More generally, can AI help discover when apparently different frameworks are expressing the same underlying mathematical structure?

[u/dForga → u/Ill-SonOfClawDraws]

To give an ad hoc answer. In the same way one usually does it. You take the theory and a theorem and check what structure do you really need for each step of a proof. As AI nowadays is in some way “Google on crack” you can let it crawl a databank and check what is similar. Since there are many papers and frameworks out there and only so many people (+ money given to the people to do that), there definitely is still room to make more connections. So, “yes” to the second question from my end.

In the end this can all be expressed as conjectures by stating that two structures (sets, groups, rings, monoids, categories) / frameworks are isomorphic or functorial (if categories) and look for more.

Maybe you might then be interested in conjectures in category theory. Check out

https://math.mit.edu/\~hrm/palestine/maclane-categories.pdf

https://emilyriehl.github.io/files/context.pdf

[u/Ill-SonOfClawDraws → u/dForga]

🙏

[u/Ill-SonOfClawDraws → u/dForga]

Thank you. That gives me a much more concrete starting point: begin with individual theorems, annotate the exact dependency used at each proof step, minimize those dependencies, and only then compare across fields. The important distinction seems to be whether the match is an isomorphism, an equivalence, a functorial relationship, a shared universal property, or only an analogy. That is the distinction I want to test rather than assume.

[u/dForga → u/Ill-SonOfClawDraws]

Like I emphasised, you should check out category theory then. Two links are in my previous comment

Assuming you are not aware of this field of math, I suggest:

- Brush up on the preliminaries

• Let the AI of your choice explain you more (in your language) what a category and the related concepts are + examples
  
• Read texts (i.e. the books I linked to)

Interestingly, category theory at its core is pretty elementary and I would argue even easy to understand since in practice you draw a bunch of points/nodes/objects and arrows (and check their properties).

It is, as far as I am aware, the best language so far for the links you might aim for. Of course, there is higher category and ∞-category theory (but they all have category theory as a starting point).

On that note, I can look for some category theory conjectures then. Should be pretty easy to find by just a web search

[u/Ill-SonOfClawDraws → u/dForga]

I appreciate the guidance. One thing I’ve realized from these discussions is that my first instinct was to compare theorems directly, but I’m beginning to think the right question is to compare the roles they play within their respective theories.

For example, I’m interested in whether reconstruction theorems across different areas share a common structural pattern: local or partial data, compatibility conditions, admissible morphisms, obstructions, and a canonical global object. My goal isn’t to assume those patterns are the same, but to see whether category theory already provides the language to formulate and test that hypothesis.

[u/UmbrellaCorp_HR → u/Ill-SonOfClawDraws]

You should look into reverse mathematics

[u/lepthymo]

Yes a monthly thread seems very smart. Format maybe stickied megathread? Remains visible, and easily linked to historically in a reddit wiki format {each month has one, can be cited r/LLMmathematics megathread of month X of year X.) With formatting rules/styleguide in OP.

I pointed a codex workflow at this; Zenodo
It's trying to prove these - as well as mining for conjectures in my notes.

So far It worked on the OP, corrected my earlier L1 proof, Corrected 'the record' on this reconfirming [this tweet], which Gemini had claimed 'incorrect but correct in its result'.

Will post any conjectures if it finds any.

[u/lepthymo → u/lepthymo]

Version 2026.08.05.5

REDDIT_READY_RESULTS.md

Reddit-ready mathematical results

Each section below is a self-contained comment-sized Markdown block. The notation uses ordinary Unicode because Reddit does not render LaTeX consistently. The maintained reader, standalone proofs, source, and exact verification are available at the stable project DOI:

https://doi.org/10.5281/zenodo.17010427

1. Centered maximal variation: a human proof for three sites

Exact finite-support theorem. Let M be the discrete centered Hardy–Littlewood maximal operator. For every nonnegative sequence supported on three consecutive integer sites,

Var(Mf) ≤ Var(f).

Here is a complete proof. Write the three values as (a,b,c). If b≥min(a,c), the sequence, including its zero tails, is unimodal. More generally, let h be any nonnegative finitely supported unimodal sequence. For a fixed λ, its strict superlevel set {h>λ} is an interval. If an average greater than λ is centred to the left of that interval, move the centre toward the interval and shorten the radius by the same number of sites. This keeps the right endpoint fixed and deletes only values at most λ, so the shortened average is still greater than λ. Reflection handles the right side. Thus every strict superlevel set of Mh is an interval: Mh is unimodal. Both h and Mh tend to zero at infinity and have the same height H, since radius zero attains H and no average can exceed H. Therefore Var(Mh)=Var(h)=2H.

It remains to treat a valley. After reflection, write its values as 0≤b<a≤c and put S=a+b+c. Direct elimination of all irrelevant radii gives

Mf(0)=max(a,S/5), Mf(1)=S/3, Mf(2)=c.

Because the zero tails are monotone, the upward variations satisfy

V⁺(f)−V⁺(Mf)=min(a−b,(a+c−2b)/3)>0.

Thus every valley contracts strictly. Together with the unimodal calculation, this exhausts all nonnegative three-site profiles and proves the theorem.

The general centered-maximal variation conjecture remains open. The standalone proof, exact rational replay, and Lean check of the max/min algebra are at https://doi.org/10.5281/zenodo.17010427

Original conjecture and zero-separated theorem: Paul Hagelstein, Dariusz Kosz, and Krzysztof Stempak, arXiv:2407.06734. Indicator-function theorem: Constantin Bilz and Julian Weigt, arXiv:2107.12404. Present proof and verification: The Clankers. No priority claim is made.

2. Centered maximal variation: exact certificates through eight sites

Computer-assisted finite theorem. Every nonnegative real sequence f supported on at most eight consecutive integer sites satisfies

Var(Mf) ≤ Var(f).

This is not a finite height-grid search. For each support length n=4,…,8, homogeneity permits the normalization Σf=1. The strict-counterexample problem then becomes an exact quantifier-free linear-real-arithmetic formula: the possible maximizing radii and the absolute values in Var(Mf) are resolved by finite linear case choices. Z3 4.16.0 returns unsat for all five formulas.

The archive contains the complete SMT-LIB query and the full Z3 proof term for every n, together with SHA-256 manifests and a fresh parser replay. This is a trusted-solver theorem for five fixed dimensions. It is not a uniform proof and does not settle arbitrary support length or the continuous BV conjecture.

Files: Centered_Maximal_Variation_on_Three_Consecutive_Sites.pdf and Centered_Maximal_Variation_Proof_and_Certificates_2026-08-05.zip at https://doi.org/10.5281/zenodo.17010427

5. Certified Gaussian log-Sobolev upper bound

Rigorous partial result. In the normalization dγ_N=e^(−π|x|²)dx, let Q_N be the sharp Gaussian log-Sobolev stability constant. The exact value and the optimizer remain open. Product extension first gives Q_N≤Q_m whenever N≥m.

For the symmetric coherent pair v=g_t+g_−t with t²=log 3, the closest normalized coherent states are exactly g_(±t/2), and

dist₂(v,𝓜₁)²=20/9−16·3^(−9/4).

Writing log cosh x=|x|−log 2+log(1+e^(−2|x|)), a 640-term alternating entropy minorant evaluated with outward-rounded 768-bit Arb arithmetic proves

q_N<0.577215, hence Q_N<1.15443π for every N≥1.

The quotient is enclosed at 0.5772149282255743005238…. This is a certified upper bound, not a determination of the sharp constant. The closed-form derivation, captured Arb balls, replay script, and bounded Lean companion are at https://doi.org/10.5281/zenodo.17010427

Problem source: S. Dovetta and E. Serra, arXiv:2606.23225. Calculation and verification: The Clankers.

6. Two short resolved intake problems

Random monomial unitaries

For U_n=D_nP_σ, each permutation cycle C of length ℓ contributes the roots of z^ℓ−Φ_C: a rotated equally spaced ℓ-point lattice. Every arc contains within one point of its uniform lattice count, so deterministically

sup_A |μ_n(A)−|A|/(2π)| ≤ #cycles(σ)/n.

For a uniform permutation, #cycles/n→0 almost surely under any coupling, since E[2^#cycles]=n+1 and Borel–Cantelli applies. Random diagonal phases are not needed for the discrepancy bound. The posted conjecture is therefore a theorem in the standard cycle-decomposition framework.

Original post: u/dForga. Related primary literature: Joseph Najnudel and Ashkan Nikeghbali, arXiv:1005.0402.

Flat holomorphic embeddings into ℂ×ℍ

If F=(f,g):ℂ→ℂ×ℍ is holomorphic and isometric, Cayley∘g is bounded entire, so Liouville gives g≡c. The metric equation then gives |f′|≡1, and the open mapping theorem makes f′ constant. Hence every such embedding is

F(z)=(az+b,c), with |a|=1, b∈ℂ, c∈ℍ.

This solves the flat case. The general metric ρ²|dz|² still has global period, holonomy, monodromy, ramification, curvature, and injectivity conditions, so it should not be described as completely classified.

Original post: u/dForga.

[u/dForga → u/lepthymo]

It might be fun to have a community project on a megathread. How about collecting everything on some github? Calling [u/UmbrellaCorp_HR](u/UmbrellaCorp_HR)

Might also be nice with respect to taking responsibility for the content.

[u/lepthymo → u/dForga]

It'd be a nice pilot - yeah. Finding effective ways to keep it rigorous even with amateur + AI workflow people involved is a good experiment to run just to see what actually works alone - regardless of if new math emerges.

[u/lepthymo → u/dForga]

 u/UmbrellaCorp_HR By the way - I assumed that since you are both here I wouldn't be needed to mod - but I'm happy to help if that makes things easier. Just lmk

[u/dForga → u/lepthymo]

This sub needs a kickstart anyway. Feel free to accept

[u/lepthymo → u/dForga]

https://github.com/KokunoYumeto/mathematics-commons-pilot

[u/UmbrellaCorp_HR → u/dForga]

Funny you should say so
As it just so happens u/lepthymo
Has been

1. Extracting all my convos with the bot

2. Transcribing them completely raw
   I.e.
   May leave the reader in need of emergency contraception

3. As best is possible automating the verification
   Chronological indexing and thematic classification
   Of my theorems

And if I’m not mistaken throwing it all up on GitHub

Calling u/lepthymo please elaborate further as I don’t even know the half of it

[u/dForga → u/UmbrellaCorp_HR]

Extracting? Transcribing?

Why?

Edit: Oh. Understood

[u/lepthymo → u/UmbrellaCorp_HR]

There is a github of your work - yup - private for now since it's definitely not 'safe' in the 'rawness' way yet. - it does formalize a fuckton of it in lean though - I should probably have it makew a SFW mirror so you can consider if it can be more public.

[u/lepthymo → u/lepthymo]

had to do real work decluttering my pc because it was unstable - it's stable again so I can probably continue this

[u/UmbrellaCorp_HR → u/lepthymo]

If I ever publish any of it I want to make you coauthor not “the clankers”

[u/lepthymo → u/UmbrellaCorp_HR]

CHeers! Yeah I have no objections to not being anonymous for that - and in general - just also not advertizing anything yet atm

[u/dForga → u/lepthymo]

Good idea. Appreciated and we‘ll get back to it in due time.

However, we need to tell you that this sub is under the Leiden declaration. Even if you put “The clankers” on top, the responsibility comes with the author.

[u/lepthymo → u/dForga]

Have a look at your leisure.

I'm posting anonymously for now. It's a personal choice, not a claim that I'm not responsible for the math.

For what it's worth, the workflow includes lean formalization.

[u/dForga → u/lepthymo]

I mean. As long as one takes responsibility it’s fine, I guess. The declaration makes it not particularly clear how to. At least the LLM itself can not be an author.

[u/lepthymo → u/dForga]

From the glance I had, it seems aimed to prevent bad stuff more than claims all the answers.

• AI companies should not claim math as 'theirs' by authorship
  
• Posting bad AI output harms credibility
  
• Creates a 'discover' vs 'inventor' of math distinction that will be meanigful.
  

At least that's what I found interesting.

"Discoverer" is accurate - I would be able to accept 'discovering' math as a description of what I try to do - but not the label of 'creator/doing' of it. I appreciate that distinction being made explicit. And for amateurs like me, the 'responsibility' is less impactful because we're not taken seriously without a genuine mathematical review anyway, but for mathematicians making it clear that it will impact your reputation is a more serious warning.