Currently explicit formally verifiable proofs provide no value for most mathematicians apart from some specific fields. This may gradually change if proof assi

Currently explicit formally verifiable proofs provide no value for most mathematicians apart from some specific fields. This may gradually change if proof assistants and proof checkers improve. It may become to incorporate some machine learning aspects and let algorithms search proof space that is too tedious for humans. This would finally turn computer into bicycle for mathematician.