Автоматизирано разсъждение (Automated Reasoning)

Автоматизираното разсъждение е клон на изкуствения интелект и математическата логика, занимаващ се с проектирането на компютърни програми, способни да правят логически изводи и да доказват теореми.

Чрез обединяване на невронни мрежи, генериращи математически хипотези, с детерминистични формални верификатори (като Lean или Isabelle), автоматизираното разсъждение отваря врати към откриване на нови математически истини.