I'm still trying to understand it cuz I just found out about this today but, very briefly, Metamath is a project to define all of mathematics from foundations to higher-level concepts via a formal language for defining formal languages. So basically, you can look at any given mathematical theorem and find a series of rules that rewrite it down to the most basic axioms of math (they have a system based on the more traditional branch of math based on classical first-order logic and ZFC set theory and also some intuitionist system I don't really know about)

It's rly cool, highly recommend checking their web-based proof explorer out if you want to get into abstract math but it seems overwhelming or you don't know where to start. If you are into math you might find it extremely verbose but that's the price to pay for such a rigorous, formally defined, system lol

I was trying to write a proof for a thing based on a bit about probability theory I saw here lol, I think my proof is feasible in theory but I haven't figured out how to get it to work in Metamath (interestingly it's directly connected with that 0.999... = 1 thing lol)

I think proof assistants and automated theorem prover programs are really cool, is there any more computer math stuff I should know about? I don't know anything about abstract math tbh, but I want to if I can (I am also limited by not rly being into lambda calculus stuff lol and running OpenBSD)