A Formal Axiomatization of Computation
This work addresses a foundational problem in theoretical computer science by providing a new axiomatic approach to computation, potentially impacting all of ML/AI, but it is incremental as it builds on existing intuitionistic frameworks.
The authors tackled the problem of formalizing computation by introducing an axiomatization based on Brouwer choice sequences, and they constructed a model E that satisfies these axioms and proves P ≠ NP, showing that P is not equal to NP from an intuitionistic viewpoint.
We introduce an axiomatization for the notion of computation. Based on the idea of Brouwer choice sequences, we construct a model, denoted by $E$, which satisfies our axioms and $E \models \mathrm{ P \neq NP}$. In other words, regarding "effective computability" in Brouwer intuitionism viewpoint, we show $\mathrm{ P \neq NP}$.