Very Weak Subintuitionistic

Formalization of very weak subintuitionstic logics in Lean 4.

Status: WIP: This formalization is migrated from old codes from Foundation. Currently we are rewriting proofs for more generalized results on latest articles.

Related Articles

1. Taishi Kurahashi, Mashi Noguchi, Very weak subintuitionistic logics, 2026/05, arXiv:2605.20769.

Authors

• Mashu Noguchi (@SnO2WMaN)

License

This project licensed under CC-BY-SA 4.0. See LICENSE.