to be really pedantic, I'd say PoS is an economic breakthrough rather than heavy-duty computer science, strictly speaking. the actual math of the consensus algorithms seems relatively simple, the challenge is aligning all the incentives so that adversaries in a group of anonymous people have nothing to gain by subverting the rules.
I will gladly give a Turing award to whoever formally proves the safety and liveness of Gasper like Lamport did for Paxos.
I will gladly give a Turing award to whoever formally proves the safety and liveness of Gasper like Lamport did for Paxos.