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

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