# How do I get back into math?

## This page summarizes the projects mentioned and recommended in the original post on reddit.com/r/math #programming-language #theorem-proving #type-theory #Verification #Dependent Types Post date: 26 Mar 2021

• Scout APM - Less time debugging, more time building
• JetBrains - Developer Ecosystem Survey 2022
• SonarQube - Static code analysis for 29 languages.
• ### OEISbot

Automatically posts links to OEIS sequences on Reddit

I've just put in a pull request to OEISbot on Github to fix this.

• ### lean

Lean Theorem Prover (by leanprover)

However, mathlib makes some weird design choices. For example, (semi)groups are defined using multiplicative notation -- and then immediately followed by an entire section giving the exact same definitions using additive notation! The claimed reason for this is that the more abstract approach is inconvenient for automation. I did it in Coq using the abstract approach, and indeed, noticed that doing so broke automation, which I then worked around in various ways. But it's just weird to me as a mathematician to have additive and multiplicative groups be different objects, so I wouldn't want to do it the Lean way come hell or high water. The Lean approach causes practical difficulties as well: you have to prove every theorem about groups twice. In some cases (e.g. product groups), you have to prove every theorem FOUR times. Ugh.

• ### Scout APM

Less time debugging, more time building. Scout APM allows you to find and fix performance issues with no hassle. Now with error monitoring and ﻿external services monitoring, Scout is a developer's best friend when it comes to application development.

• ### arend-lib

Formal proofs are fine, only tactics proofs are awkward. For example, with tactics https://wwwf.imperial.ac.uk/%7Ebuzzard/xena/natural_number_game/?world=9&level=4 is a challenge that requires a logical trick. But as a functional programming style proof it's completely straightforward: https://github.com/JetBrains/arend-lib/blob/master/src/Arith/Nat.ard#L126

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.