Less computers! More blackboards!

I'm currently doing an internship in a computer science research institute.

Actually we don't have blackboards, but white. And I still don't have my office, anyway.


During the next 5 months, I'm going to try to formalize the transformation of information in proof theory, with category theory as an approach of graph transformation.
Ok, that pretty much the title... I gonna try to explain that.

Concretely, a proof is a tree.
At the top, the leaves are the hypotheses, your materials to prove something.
Could be statements, or theorem already proved as inference rules.
And at the bottom, the root is what you want to prove, as a goal. A new brand theorem.
You combine hypotheses. Get new ones, given by application of intermediate theorems.
Until your goal pops out of all of these actions.

Every manipulations of your hypotheses, to reach your goal, is a transformation of the tree.
Mostly relations between hypotheses and theorems applied, to get sub goals.
A mini proof tree in the proof tree.

There is a field of computer science which formalizes transformation of information. With category theory on graph theory.
But it's another story, another day.

By now, I'm only reading past publications of my supervisors, or their phd students.
In march I'll start to take some exemples of proofs, simple ones, and formalize the transformations made to get the proof.
It's just pure gold...