One day I realized that the Strong Goldbach Conjecture could actually be stably situated within the level of Second-Order Logic (SOL)—as long as we don’t try to prove it, and instead only require semantic closure.
Then I found a way to bypass that and shift the formulation into Higher-Order Logic (HOL). After some research, it seemed this could potentially be handed over to AI systems for reasoning.
However, when it comes to implementing it in Coq or other formal systems, that’s beyond my expertise. That’s why I wrote this article—to document the idea and invite others to explore.
The formulas in the article were verified multiple times using GPT, but have not been reviewed by human experts.
Then I found a way to bypass that and shift the formulation into Higher-Order Logic (HOL). After some research, it seemed this could potentially be handed over to AI systems for reasoning.
However, when it comes to implementing it in Coq or other formal systems, that’s beyond my expertise. That’s why I wrote this article—to document the idea and invite others to explore.
The formulas in the article were verified multiple times using GPT, but have not been reviewed by human experts.