HackerPapers

arXiv:1404.6186cs.LO

ProofPeer: Collaborative Theorem Proving

Steven Obua, Jacques Fleuriot, Phil Scott, David Aspinall

Abstract

We define the concept of collaborative theorem proving and outline our plan to make it a reality. We believe that a successful implementation of collaborative theorem proving is a necessary prerequisite for the formal verification of large systems.

arXiv comments
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 2 identifiable commenters in 2 comments across 2 threads, from May 2016 to Apr 2024.

Comments linking this paper, per year.

Discussed in comments2 threads

  1. New Foundations is consistent – a difficult mathematical proof proved using Lean 1 comment

    • Yes, this idea of collaborative proofs has been around for a while now, at least for 10 years: https://arxiv.org/abs/1404.6186

      practalView on HNParent context

  2. HARC 1 comment

    • Very exciting. I wished there would also be room for a group at YCR/HARC working on collaborative theorem proving (CTP) as proposed here: http://arxiv.org/abs/1404.6186 :-)

      auggieroseView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.