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

papers of Per Martin Löf

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

この理論は、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.

このリポジトリは、コラッツ予想に対する構成的完全証明を示します。あらゆる自然数が、特定の再帰的変換を経て最終的に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 and complete proof of the Littlewood Conjecture using structured prime density, convergence restrictions, and constructive fluctuation bounds.

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.

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