rml, (edited )
@rml@functional.cafe avatar

"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way."

  • Jacob Lurie

https://www.youtube.com/watch?v=eNgUQlpc1m0

#theoremprovers #coq #agda #lean #mathematics #hott

rml,
@rml@functional.cafe avatar

also worth noting the discussion between Lurie, Urs Schreiber, and others in the comments of this post on Mathematics Without Apologies, one of the more epic flame wars in internet history

https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/

  • All
  • Subscribed
  • Moderated
  • Favorites
  • mathematics
  • ngwrru68w68
  • rosin
  • GTA5RPClips
  • osvaldo12
  • love
  • Youngstown
  • slotface
  • khanakhh
  • everett
  • kavyap
  • mdbf
  • DreamBathrooms
  • thenastyranch
  • magazineikmin
  • megavids
  • InstantRegret
  • normalnudes
  • tacticalgear
  • cubers
  • ethstaker
  • modclub
  • cisconetworking
  • Durango
  • anitta
  • Leos
  • tester
  • provamag3
  • JUstTest
  • All magazines