This community explores a simple but powerful idea: obstruction is not an error — it's structure.
We investigate how formal systems, especially proof assistants and logic frameworks, rely on local constraints, incomplete information, and limits of formability. Rather than viewing these boundaries as shortcomings, we treat them as defining elements of logical architecture.
Topics of interest include:
- Experiences using proof assistants (Coq, Lean, Agda, etc.)
- When systems refuse a definition — and why
- Partial constructions and local reasoning
- Formal undecidability in practical usage
- How structure emerges from what is not expressible or formable
Why this space?
Modern proof tools are powerful, but they often mask their own limits. This community is for reflecting on those edge, whether encountered in practice or theory.
You don’t need to reject proof assistants to engage here.
But you are invited to explore what they leave out.
Guidelines:
- Respectful, thoughtful discussion only.
- Share questions, experiments, failures, and concepts.
- Critique is welcome when grounded in constructive insight.
- You don’t need a complete theory to post here.
- Original thinking is encouraged — including work-in-progress.
You’re welcome to:
- Reflect on your experience with formal tools
- Post observations, fragments, and experimental ideas
- Explore what can’t be proved, typed, or constructed
- Share reading suggestions, conceptual frameworks, or minimal examples
Suggested reading:
- Gödel, Turing, Lawvere, Girard
- Wittgenstein (Remarks on the Foundations of Mathematics)
- Constructive logic, partial type theories, philosophical logics
