Look into Theorem Proving in Lean

[Daniel-Mietchen]

as per https://leanprover.github.io/theorem_proving_in_lean/ — a software to model maths problems

Seen via The Mathematical Library of the Future:

For decades, mathematicians have used computer programs known as proof assistants to help them write proofs — but the humans have always guided the process, choosing the proof’s overall strategy and approach. That may soon change. Many mathematicians are excited about a proof assistant called Lean, an efficient and addictive proof assistant that could one day help tackle major problems. First, though, mathematicians must digitize thousands of years of mathematical knowledge, much of it unwritten, into a form Lean can process. Researchers have already encoded some of the most complicated mathematical ideas, proving in theory that the software can handle the hard stuff. Now it’s just a question of filling in the rest.

[Daniel-Mietchen]

There is also https://en.wikipedia.org/wiki/Lean_(proof_assistant) .

[carlinmack]

I'm doing my undergrad project in this space, but for Isabelle instead :) This article is a good starting point for the history of formalised mathematics https://en.wikipedia.org/wiki/QED_manifesto