Checks of your values and exact values at Z(12,19–21)

[nakonechnyidmitry-lab]

Hi Dylan,

I have been working on the same finite (Z(m,n;3,3)) frontier at around the same time as you were doing it.

In the beginning I used LLMs, organizing some pipelines for this Search. And (I find this funny) they tried to steal some of your values and make it sound like they "proved" :)
Later, I made enough understanding and implemented many ideas (+optimizations) on my own, including ML-based estimator of time required for SAT-solving, so managed to

My repository contains SAT/Cube-and-Conquer proofs with LRAT checking for two values also established in your repository:
(Z(9,23;3,3)=103)
(Z(10,22;3,3)=110)
(These provide a complementary verification route to your arithmetic/Lean proofs)

I also have:
(Z(12,19;3,3)=114): UNSAT at 115 plus a 114-one witness;
(Z(12,21;3,3)=126): UNSAT at 127 plus a 126-one witness;
(Z(12,20;3,3)=120): got by deletion lemma from the two adjacent
Your docs/NEW_BOUNDS.md currently lists these three cells as intervals, but maybe after some audit (that I will truly appreciate) they can be included into your table.

Repository: https://github.com/nakonechnyidmitry-lab/zarankevich_public
I can add archive/Zenodo links, e.g. https://zenodo.org/records/21215250 is storing (12; 21) and (12; 19) UNSAT's.

If you want, I can try to generate upper-bound certificates for other values
I am also interested whether you're using your own computational powers or some of Figma's too? Or you considered other options - if yes - which ones?

Best wishes,
Dmitry Nakonechnyi

[nakonechnyidmitry-lab]

(Is it interesting for you to write a real math article together? I can endure both routine and rigorous-math parts; I also made some breakthrough in ML-based estimation of solving time, can systematize methods stated in our works and use it to make true novelty for math)