Step 7 of "Proof Chain for the 24000/10451 Zero-Density Bound (Friendly Version)" (https://doi.org/10.13140/RG.2.2.11136.60161) is the key to achieve a very small, yet interesting improvement in the 30/13 Zero-Density Bound of Guth-Maynard. And I will never tire of saying it: what matters here is not the numerical improvement itself, but the technique used to achieve it.
This approach can be extrapolated to other mathematical problems that reflect onto physics, engineering, medicine, biology, and so on. In certain fields, even a minor numerical improvement can mean the difference between success and failure. Furthermore, this technique could be a game-changer for computing systems performing calculations similar to those used by Guth-Maynard, especially if they are recursive, where errors can propagate or accumulate, or where the full potential of the computation is simply not being maximized.
If proven effective in improving something as demanding as calculating the 30/13 bound, we will be looking at a highly useful tool for the entire scientific community. I am enthusiastically working to verify this work in Lean, but my resources are ridiculously limited. If anyone with computational power is willing to help, please contact me so we can team up. The verification is progressing well (considering Lean's limitations within this specific scope...), but it is slow. It is a pity, given the magnitude of this achievement and how much could be learned from this new tool.
#numbertheory #lean #lean4 #aiResearch