Open research library
Papers you can read, cite and question
609 papers from the QNFO program, filed on nine shelves by the reader each one is written for: energy per answer, error correction, physics, numbers and p-adics, logic and formalism, AI and knowledge, autonomous systems, assessments, and cross-cutting essays. Every page renders its mathematics and can be questioned in place. How a living paper works.
Looking for an answer rather than a paper? Ask the whole corpus: answers cite the papers they come from.
Proof assistants papers 10 papers
Proof assistants. Machine-checked proofs (Lean, Isabelle, Coq) Tagged papers: 10.
Hindsight Hierarchies for Reasoning Models: A Quantitative Yield and Trajectory Analysis of the Reverse-Engineering Self-Improvement Loop
Reasoning models for formal mathematics hit a data wall: training corpora consist of problems paired with machine-checked solutions, so problems beyond a model's current ability yield no solved examples, and the corpus stops growing exactly where improvement is needed. The hindsight-hierarchies…
The Zero-Point Phase as an Archimedean Factor of Weil-Index Reciprocity: A Formal Verification and Its Limits
The vacuum phase of the harmonic oscillator — the Archimedean Maslov (metaplectic) phase $e^{i\pi/4}$ accompanying the zero-point energy $\tfrac{1}{2}\hbar\omega$ — is conventionally treated as a purely real-place, analytic structure. We investigate the conjecture that this phase is instead one…
One Metalogic, Many Logics: A Quantitative Pedagogical Framework for Proof-Assistant-Based Logic Teaching with LogiKEy
Teaching logic to mixed cohorts of computer science, mathematics, and philosophy students is difficult because each cohort brings different expectations and because the standard curriculum fragments into isolated courses on propositional, modal, epistemic, and deontic logic. The LogiKEy methodology…
Degree Bounds as a First Exercise in Isabelle/ML Metaprogramming: A Reconciled Study of the poly_degree Command
Metaprogramming—writing programs that manipulate the objects, proofs, and tactics of a proof assistant itself—is a notorious barrier to entry for formal-methods newcomers, particularly mathematicians trained in classical rather than computational thinking. This paper presents a structured,…
Functorial Characterization of the Prime Numbers
This paper presents a complete theoretical characterization of the set of prime numbers, \(\mathcal{P}\), by demonstrating that it is the geometric support of a canonical object constructed via a three-stage functorial lift. This process begins in the logical stratum of Homotopy Type Theory (HoTT),…
Identity of Zero
This document presents a formal analysis of the identity of zero across mathematical, logical, informational, and physical domains. This work rejects the notion of zero as “nothingness,” proposing instead that zero is a dynamic void—a structured, operational concept whose properties are not…
The Ultimate Reality Framework Examination (URFE)
The Ultimate Reality Framework Examination (URFE) is a rigorous protocol designed to assess the comprehensiveness, consistency, and explanatory power of theoretical frameworks that purport to describe the fundamental nature of reality. It serves as an “ultimate intellectual stress test,” demanding…
Proof-of-Concept for Auditable Attention using Ultrametric Tree Distances
The dominance of high-dimensional Euclidean vector spaces in contemporary transformer architectures has precipitated an interpretability crisis, as continuous geometric embeddings can obscure the causal mechanisms of semantic attention. This paper presents a formal proof-of-concept for a…
Automated Formal Verification and Combinatorial Reduction of Distinction-Based Calculus
The foundation of modern formal mathematics has historically rested upon Zermelo-Fraenkel set theory with the Axiom of Choice (ZFC), a container-based ontology that often conflates zero with the empty set and necessitates arbitrary constraints to prevent self-reference. To systematically evaluate…
Philosophy of Science
Previous chapters have critically examined the foundations of modern physics, revealing deep challenges to our understanding of reality, substance, causality, structure, methodology, and even the process of scientific knowing itself. These challenges suggest limitations in our current scientific…
New papers by email
One short weekly digest: titles and links. No tracking; unsubscribe any time.