constructive-mathematics

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.

The mass gap over the compact simple groups

HoTT Reals in Cubical Agda

Reifying dynamical algebra: maximal ideals in countable rings, constructively

Lean 4 formalization surface; current metrics and trusted-base details live in the Release Manifest.

Proof assistant for realizability logic TCF

Axiom provenance for Lean 4 and Metamath — which step introduced an axiom, and whether the theorem statement required it Website: https://f-keys.com/gonzalgo/

Codeforces solutions pushed by CFPusher

Constructive Agda development of Echo Types: proof-relevant fibers as typed witnesses for structured information loss under non-injective maps. Provides a mechanised loss taxonomy, separation proofs distinguishing Echo from Shannon entropy and resource grades, and audience surfaces for provenance, security, and sensitivity analysis.

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

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 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.

A high-performance Rust and WebGPU engine that compiles and executes experimental logic at hardware speed.

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つの素数の和で表現可能であることを証明。再現性と拡張性を兼ね備えた数論的基盤を提供します。

このリポジトリは、コラッツ予想に対する構成的完全証明を示します。あらゆる自然数が、特定の再帰的変換を経て最終的に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.

A Constructive Formalization of Discrete Entanglement-Geometry Duality in Cubical Agda

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

Markov normal algorithms are exactly the partial recursive functions: a Lean 4 formalization with two independent proofs of the compilation direction