Add mgignoux/lean4-gl-coalgebras to bibliography (#18)

* Initial plan

* Add mgignoux lean4-gl-coalgebras to bibliography

Agent-Logs-Url: https://github.com/FormalizedFormalLogic/awesome-logic-formalization/sessions/ca1a8b5d-6347-44fc-86e9-23e6a0a64b13

Co-authored-by: SnO2WMaN <15155608+SnO2WMaN@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: SnO2WMaN <15155608+SnO2WMaN@users.noreply.github.com>

Author: Copilot

ALF/Authors.lean

@@ -129,6 +129,11 @@ def «Malvin Gattinger» : Author where
   realname := "Malvin Gattinger"
   github := "m4lvin"
 
+def «Madeleine Gignoux» : Author where
+  handle := "mgignoux"
+  realname := "Madeleine Gignoux"
+  github := "mgignoux"
+
 end Authors
 
 end

ALF/Bibliography.lean

@@ -477,6 +477,17 @@ def «m4lvin/tablean» : Repository where
   tags := [.modal_logic, .tableaux, .interpolation]
   description := "Formalisation of a tableau system for modal logic, with soundness, completeness and interpolation."
 
+def «mgignoux/lean4-gl-coalgebras» : Repository where
+  url := .mk "mgignoux" "lean4-gl-coalgebras"
+  tp := [.Lean4]
+  authors := [«Madeleine Gignoux»]
+  tags := [
+    .modal_logic,
+    .provability_logic,
+    .interpolation
+  ]
+  description := "Lean4 mechanization of modal logic GL via coalgebraic proofs, including completeness, interpolation, and fixed-point theorems."
+
 end
 
 end Bibliography
@@ -511,5 +522,6 @@ public def bibliography : List Bibliography := ([
   «Popescu Traytel 2019»,
   «Popescu Traytel 2021»,
   «m4lvin/tablean»,
+  «mgignoux/lean4-gl-coalgebras»,
 ] : List Bibliography)
 |>.mergeSort (fun a b => String.le a.slug.toLower b.slug.toLower)