Alas, not having had the time to fully read yet, but starting at the "Axiom rule" part, a strong feeling starts popping up that this is Lean, but with mathy symbols. I don't know if the intuition will hold on further reading, but there was a strong "I've seen you in a different trench coat" feeling.
Sequent calculus is way older than Lean or any similar such language. It's a bit like saying "this looks like Haskell" when reading about the Lambda Calculus.