Automatic diagram chasing in double complex

Stream: maths

[yannis monbru]

Hi, i did a research internship with Johan Commelin at the Math Institute of Freiburg for the M1 Hadamard ENS-Paris-Saclay. The topic was automatic diagram chasing.

At the end i manage to have something working for the double chain complexes by using the salamander lemma. The final result is a notebook able to state and print proofs (if you are interested you can find the code in https://github.com/ymonbru/Diagram-chasing)

For the moment the proof are pen and paper like (and mostly unreadable from a global point of view), further work is to produce a text that a proof assistant can check.

At 10h30 (UTC+2) i am giving a talk explaining how went the internship, if you are interested please contact me or Johan to get a link.