Very much agreed, and V. Voevodski has expressed authentic concern from the working mathematician side that peer review needs machine help. Wiedijk writings are

Very much agreed, and V. Voevodski has expressed authentic concern from the working mathematician side that peer review needs machine help. Wiedijk writings are nice. I have taken a look at Mizar articles and they are a fantastic sample of good things already achieved. We need to close the usability gap so writing formalizations is just easier. We need a big open source project, the Linux of mathematical vernacular.