We do have automated theorem checkers that follow your idea: from a very simple set of axioms you can build higher level lemmas and proofs that are all mechanically verified by a small trusted logical code. Its actually a very rich and fruitful research area that also happens to live quite close to computer science! Many of these proof checkers are actually just programming languages with a very fancy type system.
However, I don't think we will ever see math move to a totally computer-verified schema like you mentioned:
* First of all, its very hard to write the rigorous proofs that can satisfy a computer. Do you know that feeling when you know that your program will run just fine but the type checker is being picky about a technicality and wont accept it, meaning you need to refactor lots of stuff to appease it? Mechanically verified proofs are like that but the typechecker is even pickier!
* Often, there is a big disconnect between the important mathematical ideas and the logical foundations they build upon. For example, differential calculus has a very simple intuition (rates of change, areas under curves, etc) and can quickly biuld into applications, but its actually pretty hard to build it from basic principles. In fact, it took hundreds of years until mathematicians finally figure that part out and in the end the foundations were totally different from what they were when they started. If you tried to model this in a computer, the effect would be having to rewrite all the foundational proofs and breaks tons of interfaces and higher level lemmas as people started to learn about all the corner cases in the system.
However, I don't think we will ever see math move to a totally computer-verified schema like you mentioned:
* First of all, its very hard to write the rigorous proofs that can satisfy a computer. Do you know that feeling when you know that your program will run just fine but the type checker is being picky about a technicality and wont accept it, meaning you need to refactor lots of stuff to appease it? Mechanically verified proofs are like that but the typechecker is even pickier!
* Often, there is a big disconnect between the important mathematical ideas and the logical foundations they build upon. For example, differential calculus has a very simple intuition (rates of change, areas under curves, etc) and can quickly biuld into applications, but its actually pretty hard to build it from basic principles. In fact, it took hundreds of years until mathematicians finally figure that part out and in the end the foundations were totally different from what they were when they started. If you tried to model this in a computer, the effect would be having to rewrite all the foundational proofs and breaks tons of interfaces and higher level lemmas as people started to learn about all the corner cases in the system.