ZURAB JANELIDZE'S BLOG

Background The goal of this project is to build a proof assistant based on the SOFiA proof system, where the capital letters in SOFiA stands for Synaptic First Order Assembler (the purpose of the lower-case "i" will be explained further below) .  The use of terms "synapsis" and "assembler" is a suggestion of Brandon Laing, who wrote an MSc Thesis, "Sketching SOFiA" (2020), where the notion of an assembler was introduced: an assembler is the monoid of words in a given alphabet, seen as a monoidal category. The main result of his MSc Thesis was a characterization of assemblers using intrinsic properties of a monoidal category. An assembler gives a robust theoretical framework which guides the syntactical structure of the SOFiA proof system. The latter has been refined through a series of discussions with Louise Beyers and Gregor Feierabend in 2021, after which the first computer implementation of the SOFiA proof system was produced, based on the Py...

The bracket notion for mathematical proofs is an adaptation of the Fitch notation for Gentzen's natural deduction proof system. It has led to the development of the SOFiA proof assistant. This post brings together some videos explaining the bracket notation and the first-order formal language for mathematics in the context of the bracket notation. 1. General Overview ~ 20 min 2. Building Blocks for Statements ~ 1 hour 3. Examples of Forming Statements ~ 40 min 4. Examples of Forming Statements (Continued) ~ 35 min 5. Concluding Quantified Statements ~ 35 min 6. Concluding from Quantified Statements ~ 1 hour

Here you will find the content for the Category Theory course given under the National Graduate Academy NGA-Coursework of the CoE-MaSS . The lectures are on Saturdays 9:00-11:00.  Register here to receive the Zoom link for joining the lectures There is also a Discord channel for this course, which you can find on the Discord server  of the NGA-Coursework project.  This is a video-based course aimed at post-graduate students and as well academics interested to learn about category theory, with live participation of the audience shaping the content of the course. For a reading course at the South African honors level, see: Category Theory: A First Course  by George Janelidze For an introduction to category theory for non-mathematicians and undergraduate students, see: Elementary Introduction to Category Theory  by Amartya Goswami and Zurab Janelidze  Lecture 1: Categories Lecture 2: Functors Lecture 3: Natural Transformations Lecture 4: Adjunctions Lect...

This page contains resources for a SATACS course at NITheCS that runs over the second semester of 2022. The lectures take place on Zoom on Fridays 17:00-19:00. If you would like to join them, register here . Lecture 1: Magmas Lecture 2: Join Semi-Lattices Lecture 3: Relations Lecture 4: Universes Lecture 5: Posets Lecture 6: Groups Lecture 7: Topological Spaces Lecture 8: Posets II Lecture 9: Posets III

This is the blog post of the 2022 August NITheCS Mini-School. Let us begin with some useful links: Lecture notes on universes of sets (introductory)   Some videos explaining the concepts from the lecture notes above Lecture 1 Lecture 2 Lecture 3 Lecture 4