10
votes
4answers
1k views

Does formalizing math require search and creativity, or is it near-mechanical?

I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept. Is this type of conversion something that ...
3
votes
1answer
885 views

Proving inequalities over algebraic structures

I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the newring tactic described here for proving equalities over ...
5
votes
1answer
952 views

Is there a known way to formalise notion that certain theorems are essential ones?

Suppose You ask a question beginning from "Why some structure is..." or "Why some object has property..." and several answers arises. Which criteria do You use to qualify which answer is correct? ...