BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Gr.IV seminar: Christoph Stephan - "Formalizing Noncommutative Geo
 metry: Proof assistants\, knowledge graphs and AI in research"
DTSTART:20260218T150000Z
DTEND:20260218T160000Z
DTSTAMP:20260509T132700Z
UID:indico-event-49101@agenda.infn.it
DESCRIPTION:I will give a short introduction to Lean 4 - a proof assistant
  - and provide an overview of dependent type theory\, which underlies its 
 verification capabilities. I will then present project to formalise noncom
 mutative geometry (NCG) in Lean 4 where the long-term goal is the formaliz
 ation of Connes’ Reconstruction Theorem. While our project is still in i
 ts early stages\, the Lean community has already laid some of the necessar
 y foundations. Lean allows mathematical work to be divided into small\, v
 erifiable components\, making collaborative research more efficient. To su
 pport this process\, we are developing tools that assist with proof transl
 ation and organization of formalized results. AI is one component of these
  tools\, helping to automate and streamline certain tasks.\n\nhttps://agen
 da.infn.it/event/49101/
LOCATION:GEO-6 (DIP.TO DI GEOLOGIA)
URL:https://agenda.infn.it/event/49101/
END:VEVENT
END:VCALENDAR