Corpus - what we were looking for

• Check intuition that Nuprl proofs are close to human proofs

  • tactic steps correspond approximately to inferences people would take
  • steps at same level of granularity as human proof steps

• Look for evidence of concrete proof strategies and communication patterns

  • ideally, proof steps fitting the same role in a strategy are communicated in the same way

Previous slide

Next slide

Back to first slide

View graphic version