> One interesting thing about software as career followed by math classes is that there's no compiler - you can type any janky thought into LaTeX and if you don't detect that it's bogus, nothing will, until you show it to a professor.
The formal proof community is very interested in exactly this problem! It's not my specialty, but I believe that Lean (https://en.wikipedia.org/wiki/Lean_(proof_assistant)) is one of the very active communities.
I've done some intro to lean things, but no one in the maths program is into lean, so I'm just focusing on the math side. Terry Tao is big into the idea of lean tho, and combining LLMs with Lean.
> I've done some intro to lean things, but no one in the maths program is into lean, so I'm just focusing on the math side. Terry Tao is big into the idea of lean tho, and combining LLMs with Lean.
One of the best things about entering an underpopulated space is that you can become one of the leading experts very quickly. If it's something that appeals to you and fits your skill set, it might be worth investing the time to learn!
(Again, I say this as someone who's always been interested in formal proof, but haven't investigated it much myself, much less explored the merits and demerits of particular systems—so this is not an endorsement of Lean specifically, though it does seem to be one of the most active communities, which is important when you're trying to get into a topic.)
The formal proof community is very interested in exactly this problem! It's not my specialty, but I believe that Lean (https://en.wikipedia.org/wiki/Lean_(proof_assistant)) is one of the very active communities.