Axiom Bits and Proof Length: Short Review

Authors

  • Cristian Calude University of Aukland

DOI:

https://doi.org/10.70777/si.v3i3.17385

Keywords:

length of proofs;, proof speed-ups, speed-up theorems, algorithmic information theory, kolmogorov complexity, long and short proofs, chaitin

Abstract

Long proofs are an anathema to mathematicians. Proofs are compressed representations of information. If a theory lacks the information encoding the obstruction to a theorem, proofs must reconstruct it, resulting in a large length. Adding axiom bits shortens proofs precisely when those bits encode the missing obstruction. The article [9] studies the “gap” between the length of a theorem and the smallest length of its proof in a given formal system.

Author Biography

Cristian Calude, University of Aukland

I am Chair Professor of Computer Science at the University of Auckland, a member of Academia Europaea and Sigma Xi. My research centres on theoretical aspects of classical and quantum computing and randomness, philosophy, and the history of mathematics and computing.

News
  1. Elected Full Member Sigma Xi, 2024
  2. To Halt or Not to Halt? That Is the Question, World Scientific, 2024-2025 (translations in Russian and Romanian)
  3. These Are the Most Bizarre Numbers in the Universe, 2023
  4. Frontiers of Computability, Randomness, and Complexity (dedicated to the 70th birthday of Professor Cristian Calude)
  5. The 20th Edition of UCNC 2023 was dedicated to Professor Cristian Calude in recognition of his founding, in 1998, and further developing of this conference series
  6. Guest to The Third Party Show, 2023

References

K. Gödel, “On the length of proofs,” in Collected Works, Vol. I, Oxford University Press, 1986.

G. Kreisel, “On the interpretation of non-finitist proofs,” Journal of Symbolic Logic, vol. 16, pp. 241–267, 1951.

S. Cook and R. Reckhow, “The relative efficiency of propositional proof systems,” Journal of Symbolic Logic, vol. 44, no. 1, pp. 36–50, 1979.

S. R. Buss, “On Gödel’s theorems on lengths of proofs I: Number of lines and speedup for arithmetics,” Journal of Symbolic Logic, vol. 59, no. 3, pp. 737–756, 1994.

J. S. Royer, “Two recursion-theoretic characterizations of proof speed-ups,” Journal of Symbolic Logic, vol. 54, no. 3, pp. 867–883, 1989.

G. J. Chaitin, “A theory of program size formally identical to information theory,” Journal of the ACM, vol. 22, no. 3, pp. 329–340, 1975.

L. Bienvenu, A. Shen, and N. Vereshchagin, “The axiomatic power of Kolmogorov complexity,” Theory of Computing Systems, vol. 52, pp. 1–38, 2013. (Explicitly studies proof compression via complexity axioms.)

K. Gödel, “Uber formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte für Mathematik und Physik, vol. 38, pp. 173–198, 1931.

C. S. Calude, L. Staiger, “Long and short proofs,” “Bull. Math. Soc. Sci. Math. Roumanie,” Tome 65 (113), No. 2, (2022), 203–211.

Cristian Calude, University of Aukland

Downloads

Published

2026-09-25

How to Cite

Calude, C. (2026). Axiom Bits and Proof Length: Short Review. SuperIntelligence - Robotics - Safety & Alignment, 3(3). https://doi.org/10.70777/si.v3i3.17385

Issue

Vol. 3 No. 3 (2026): Frontiers: Toward AGI in Science - Math - Theorem Proving

Section

Articles

Categories

License

Copyright (c) 2026 Cristian Calude

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.