An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

Logical manifestations of topological concepts, and other things, via the univalent point of view.

Reifying dynamical algebra: maximal ideals in countable rings, constructively

Proof assistant for realizability logic TCF

delta‑analysis library – a parametric factory for producing any kind of mathematical analysis, where the continuum emerges from iterative refinement. Provides frameworks for functions on arbitrary address spaces (rationals, matrices, binary strings, p‑adic numbers, will extend) with adaptive grids, exact rational arithmetic, and rigorous calculus.

papers of Per Martin Löf

A verified constructive reduction of the Cook-Levin Theorem in Lean 4.

A tool for verifying constructive geometry problems. This repository focuses on the systematic verification of step-by-step solutions to ensure correctness and adherence to geometric principles.

このリポジトリは、コラッツ予想に対する構成的完全証明を示します。あらゆる自然数が、特定の再帰的変換を経て最終的に1へと収束することを、合同類の構造論理とループ排除の形式によって証明します。 This repository presents a constructive complete proof of the Collatz Conjecture. It shows that any natural number ultimately converges to 1 via recursive transformation, using congruence class structure and loop elimination.

This repository presents a constructive solution to the Yang–Mills existence and mass gap problem, a Clay Millennium Prize topic. The framework confirms the existence of a positive mass gap through verifiable quantum field logic. 本リポジトリでは、クレイ懸賞問題のひとつであるヤン–ミルズ存在と質量ギャップ問題に対し、構成的に正の質量ギャップの存在を示す理論を収録しています。量子場理論に基づき、検証可能な構成を整備しています。

A foundational theory redefining "existence" as quantizable via constructive logic. Applicable to AI cognition, encryption, quantum memory, and beyond. 構成的論理により「存在」を量子化可能な単位として再定義。AI認知・暗号・量子記憶など幅広い応用を想定した基礎理論です。

A constructive and complete proof of the Littlewood Conjecture using structured prime density, convergence restrictions, and constructive fluctuation bounds.

この理論は、6n±1 によって表現可能な数のうち、合成数を除去して残る純粋な素数列（A型素数）を構成的に導出する補強モデルです。暗号や数論の応用に適したA型素数を効率的に生成する新たな数論的アプローチを提供します。 This theory proposes a constructive refinement of the 6n±1 prime form by systematically eliminating composites to extract pure A-type primes, enabling efficient generation for cryptographic and theoretical applications.

A formal constructive proof of the Goldbach Conjecture using A-type primes. The theory guarantees every even number ≥4 can be expressed as a sum of two primes, offering a reproducible and extendable number-theoretical foundation. A型素数を用いた構成的手法により、すべての偶数（4以上）が2つの素数の和で表現可能であることを証明。再現性と拡張性を兼ね備えた数論的基盤を提供します。

Provide a verified, machine-checked constructive reduction of the Cook-Levin theorem from Turing machines to SAT formulas using Lean 4.

A compositional theory that unifies the proof of unsolved problems, AI structure, medical control, and physical modeling using a single constructive function C(x). 単一の構成関数C(x)により、未解決問題、AI構造、医療制御、物理モデルを統一的に証明・構成する理論です。

Stabilna wersja alfa mojej książki o Coqu, programowaniu funkcyjnym, teorii typów, logice konstruktywnej i innych dziwnych rzeczach.

Constructive proof of the Beal Conjecture using ABC-model extension and coprime domain elimination

onstructive proof of the Catalan Conjecture (Mihăilescu's Theorem)

Constructive Reverse Mathematics Series — 70 papers, ~88k lines Lean 4. The logical cost of mathematics is the logical cost of ℝ. Physics: doi.org/10.5281/zenodo.18654773 | Arithmetic: doi.org/10.5281/zenodo.18746343 | Capstone: doi.org/10.5281/zenodo.18750992