Open research library
Papers you can read, cite and question
611 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.
Logic & formalism papers 3 papers
Logicians, formal-methods and foundations readers. Formal systems and what they cannot say: Laws of Form and the calculus of indications, distinction and re-entry, self-reference, category theory, coalgebra and bisimulation, proof assistants, computability, formal ontology.
Proof assistants. Machine-checked proofs (Lean, Isabelle, Coq) Tagged papers: 10.
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,…
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…
New papers by email
One short weekly digest: titles and links. No tracking; unsubscribe any time.