Hclean Collatz Formalization Project
Formalization and Machine Verification of a Relational Proof Architecture for the Collatz Conjecture
The Hclean Collatz Formalization Project is a research program of the Sir Roger Penrose Institute for Interdisciplinary Sciences devoted to the mathematical stabilization, formalization, and machine verification of a relational proof architecture for the Collatz conjecture.
The project is based on a preliminary manuscript by Katarzyna Anna Paruzel, deposited on Zenodo as:
A Relational Proof Architecture for the Collatz Problem in the Hclean Model
DOI: 10.5281/zenodo.20733100
The current stage of the project focuses on transforming the preliminary mathematical architecture into a stabilized, independently reviewable, and eventually machine-checkable formal proof framework.
Project Overview
The Collatz conjecture is one of the most persistent open problems in elementary number theory and discrete dynamical systems. Its statement is simple, but its dynamics display highly irregular local arithmetic behavior.
The Hclean model approaches the problem from a relational perspective. Instead of treating Collatz trajectories only as isolated numerical sequences, the model reorganizes the reduced Collatz dynamics into a structured system of:
- encoded relational states,
- valuation signatures,
- residue components,
- refinement projections,
- tail families,
- family-level transitions,
- finite relational truncations,
- a distinguished relational center generated by the fixed point 1.
This relational architecture is designed to analyze the two principal global obstructions to closure:
- possible infinite growth channels;
- possible noncentral recurrent or terminal regimes distinct from closure to the classical reduced fixed point.
The Hclean approach studies these obstructions through structural mechanisms called anti-escape and anti-autonomy.
Priority Record
A preliminary priority manuscript has been publicly deposited on Zenodo:
Katarzyna Anna Paruzel
A Relational Proof Architecture for the Collatz Problem in the Hclean Model
Zenodo DOI: 10.5281/zenodo.20733100
This record establishes the public priority of the Hclean relational proof architecture and provides the initial mathematical basis for the formalization project.
The public preliminary record does not include a Lean 4 formalization. Formalization and machine verification are planned as subsequent stages of the project.
Scientific Objective
The central objective of the project is to transform the Hclean relational proof architecture into a stabilized and formally verifiable mathematical framework.
The project aims to:
- stabilize the definitions and logical dependencies of the preliminary manuscript;
- prepare the proof architecture for formal verification;
- develop a Lean 4 foundation layer for the reduced Collatz map and associated relational structures;
- formalize the core structural modules of the Hclean architecture;
- subject the proof architecture to independent mathematical review;
- prepare reproducible research outputs, including documentation and archival records.
The long-term goal is to produce a transparent and inspectable verification pathway for the Hclean approach to the reduced Collatz dynamics.
Current Status
The current public status of the project is:
- preliminary manuscript deposited on Zenodo;
- priority record established through DOI registration;
- project page created by the Sir Roger Penrose Institute for Interdisciplinary Sciences;
- formalization stage planned;
- independent mathematical review planned;
- public Lean 4 release not yet available.
The project is currently in the transition phase between preliminary mathematical architecture and formal verification planning.
Planned Formalization
The planned formalization stage will use Lean 4, a modern theorem prover and proof assistant. Lean 4 enables mathematical definitions, lemmas, theorem statements, and proofs to be expressed in a precise formal language and checked by a kernel.
The planned formalization will focus on the core proof modules of the Hclean architecture, including:
- the reduced Collatz map on positive odd integers;
- valuation signatures and residue components;
- encoded relational states;
- refinement projections and projective consistency;
- the Hclean relational graph;
- tail-family structure and family-level transitions;
- finite relational truncations;
- anti-escape reductions;
- anti-autonomy analysis;
- the final arithmetic-center bridge to the classical reduced fixed point 1.
The purpose of the formalization is not merely computational support. It is intended as a rigorous method for exposing hidden assumptions, clarifying dependencies, and transforming the preliminary architecture into a reproducible mathematical object.
Principal Investigator
Katarzyna Anna Paruzel
Founder, President of the Board, and Chief Scientist / Research Director
Sir Roger Penrose Institute for Interdisciplinary Sciences
ORCID: 0009-0003-7818-9157
Katarzyna Anna Paruzel is the author of the Hclean relational proof architecture and the Principal Investigator of the Hclean Collatz Formalization Project.
Her research focuses on fundamental physics, information theory, foundations of mathematics, discrete dynamical systems, relational models of reality, and interdisciplinary approaches to the structure of information, matter, geometry, and complexity.
Institutional Framework
The Sir Roger Penrose Institute for Interdisciplinary Sciences is a Polish research-oriented association based in Wieliczka, Poland.
The Institute develops interdisciplinary research programs in areas including:
- fundamental physics,
- cosmology,
- information theory,
- mathematical foundations,
- neuroscience,
- psychology,
- consciousness studies,
- formal and conceptual models of reality.
The Hclean Collatz Formalization Project is conducted as part of the Institute’s broader research activity devoted to formal, conceptual, and computational approaches to fundamental scientific problems.
Planned Outputs
The planned outputs of the project include:
- a stabilized version of the Hclean Collatz manuscript;
- a formalization roadmap for the core proof architecture;
- a Lean 4 repository, once the formalization reaches a release-ready stage;
- technical documentation and reproducibility instructions;
- updated Zenodo records and DOI-based archival releases;
- independent mathematical review of the proof architecture;
- conference or workshop presentations;
- a final manuscript suitable for submission to an appropriate mathematical venue.
Contact
Sir Roger Penrose Institute for Interdisciplinary Sciences
ul. Krakowska 19
32-020 Wieliczka
Poland
Email: contact@inipenrose.org
Website: https://inipenrose.org
For inquiries regarding the Hclean Collatz Formalization Project, please contact the Institute at: