From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Rusi Newsgroups: gmane.emacs.help Subject: Reality and Proofs (was if vs. when vs. and: style question) Date: Mon, 30 Mar 2015 23:26:31 -0700 (PDT) Message-ID: <34cc5b29-24c8-4b98-ad64-7e7ea503578e@googlegroups.com> References: <87lhilx0cf.fsf@debian.uxu> <87twx9360u.fsf@kuiper.lan.informatimago.com> <0d1d19ab-06e9-462d-8867-9a49b1e232d3@googlegroups.com> <87pp7x2jav.fsf@kuiper.lan.informatimago.com> <87d23s4nt4.fsf@debian.uxu> <7e8ddf8f-163a-4d16-9ce2-25b0cb3f35aa@googlegroups.com> <87sicny7zm.fsf@kuiper.lan.informatimago.com> <874mp3clqi.fsf@wanadoo.es> <20150330094432.GA30418@tuxteam.de> <87a8yuy6wn.fsf@kuiper.lan.informatimago.com> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: ger.gmane.org 1427783421 29504 80.91.229.3 (31 Mar 2015 06:30:21 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Tue, 31 Mar 2015 06:30:21 +0000 (UTC) To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Tue Mar 31 08:30:20 2015 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Ycpgn-0001UD-Ah for geh-help-gnu-emacs@m.gmane.org; Tue, 31 Mar 2015 08:30:17 +0200 Original-Received: from localhost ([::1]:37146 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Ycpgm-0000uT-FE for geh-help-gnu-emacs@m.gmane.org; Tue, 31 Mar 2015 02:30:16 -0400 X-Received: by 10.43.130.198 with SMTP id hn6mr64298425icc.29.1427783192339; Mon, 30 Mar 2015 23:26:32 -0700 (PDT) X-Received: by 10.50.119.4 with SMTP id kq4mr18177igb.0.1427783192294; Mon, 30 Mar 2015 23:26:32 -0700 (PDT) Original-Path: usenet.stanford.edu!h15no2154766igd.0!news-out.google.com!q14ni3935ign.0!nntp.google.com!h15no2154758igd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Original-Newsgroups: gnu.emacs.help In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=117.195.54.22; posting-account=mBpa7woAAAAGLEWUUKpmbxm-Quu5D8ui Original-NNTP-Posting-Host: 117.195.54.22 User-Agent: G2/1.0 Injection-Date: Tue, 31 Mar 2015 06:26:32 +0000 Original-Xref: usenet.stanford.edu gnu.emacs.help:211181 X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Xref: news.gmane.org gmane.emacs.help:103463 Archived-At: On Monday, March 30, 2015 at 8:51:47 PM UTC+5:30, Marcin Borkowski wrote: > Hello, > > first of all: I stand in awe watching this discussion I've inadvertently > started. Yes the commission of elders is deliberating on the right scale and form of punishment for this misdemeanor > > On 2015-03-30, at 16:18, Stefan Monnier wrote: > > >>> Do you know any Mathematician that is paid by the hour? ;-) > >> Or that is forced to use differential geometry to solve his problem, > >> whatever it is, because the enterprises only has other specialists of > >> differential geometry, and they are easy to find for hiring. > > > > Along the same lines, I don't know many programmers whose code is never > > passed to a compiler/interpreter but is instead only read by other > > human beings. > > BTW: I think you nailed a serious problem with contemporary mathematics: > that machine checking proofs isn't a routine part of the publishing > process. The number of erroneous papers in math journals is > horrifying. Substantial portion of my depatment's seminar is devoted to > discussing errors in papers. Once a colleague found a relatively simple > /counterexample/ to a theorem which was a cornerstone of a whole theory > (and a basis for several dozen other papers). Thomas Kuhn points out that scientific paradigms not only shift slowly with time, they may actually be incommensurable. So Galileo was wrong and the pope/ecumenical council were right in punishing Galileo for his ideas because the earth was *by definition* immovable. IOW we have a different earth today than they had. Likewise proofs/truth etc changed dramatically from Aristotle/Euclid to Galileo/Descartes/Newton and once again has seen vast changes post the computer era. Some recent thoughts collected on that subject http://blog.languager.org/2015/03/cs-history-0.html