FFL Monthly Report 2025/10

Stream: Formalized Formal Logic

[SnO2WMaN]

https://formalizedformallogic.github.io/Foundation/book/Monthly-Reports/Monthly-Report-2025___10/

Here is the progress we made in October 2025. Last month we mainly formalized the following:

• Consistency of ZFC: Lean4 ⊢ Con(ZFC) (by @Palalansoukî )
• Filtreation for neighborhood semantics for modal logic (by @SnO2WMaN )
• Interpretability logic and Veltman semantics (by @SnO2WMaN )

If you have any question, please feel free to ask.

p.s. We've created Open Collective account. Currently, this project receives little to no financial support. If you find our work valuable, please support us for helping to sustain our OSS development!