I let my bots grind on a tiny open case Knuth left behind

Question: whats the smallest circuit that tells you if the number of 1s in 6 bits is 1 mod 3?

Known answer was at most 13 gates. Nobody had pinned it down past 5 inputs

My bots split it into 3,735 SAT sub-problems and ran ~153 CPU hours on one 8 core box

Result: no 12 gate circuit exists. So the answer should be exactly 13

Not calling it proven yet. Independent review is still running. 123 of 129 sampled cubes re-solved, all UNSAT, and 118 already checked by a formally verified proof checker

Side find: smallest AND/OR formula for 5 input majority is exactly 14 leaves. Might already be known

No this doesn't solve P vs NP lol. This is just tiny exact cases on the way there 🫪