AMS Notices: A Special Issue on Formal Proof

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

AMS Notices: A Special Issue on Formal Proof

Owen Densmore
Administrator
A fascinating issue from the AMS  http://www.ams.org/notices/200811/

The preview:
     "Using computers in proofs both extends mathematics with new  
results and creates new mathematical questions about the nature and  
technique of such proofs. This special issue features a collection of  
articles by practitioners and theorists of such formal proofs which  
explore both aspects."

A problem a few of us have been discussing at The Complex is the  
division between computing and mathematics, between algorithms and  
equations.

For example: Is current mathematical notation today's roman numerals,  
a syntax we have to leave behind or enhance to integrate with  
algorithms or "scripts".

Fascinating folks in the past like Ken Iverson have made serious  
inroads with APL, a formalized mathematical computing language.  
(currently advanced by his son Ralph in a new, more modern form as J: http://www.jsoftware.com/)

     -- Owen



============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
lectures, archives, unsubscribe, maps at http://www.friam.org
Reply | Threaded
Open this post in threaded view
|

Re: AMS Notices: A Special Issue on Formal Proof

Jochen Fromm-4
nice quote

> "Is current mathematical notation today's roman numerals,  
> a syntax we have to leave behind or enhance to integrate with  
> algorithms or "scripts""
 

-J.

============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
lectures, archives, unsubscribe, maps at http://www.friam.org
Reply | Threaded
Open this post in threaded view
|

Re: AMS Notices: A Special Issue on Formal Proof

Kenneth Lloyd
Interesting quote, indeed.

I personally find it challenging to keep up with new mathematical notations.
"With every new mathematical concept comes its own new mathematical
notation." I can't remember who said it, but I find it true. I can't quite
decided whether it's the new notation, or the new concepts that cause me
fits.

Example, see Samson Abramsky's (Oxford Quantum Computing) extension of
Feynmann diagrams into a new "graphical calculus".

So I suppose I ask: "Which mathematical notations are destined for history's
dust bin?"

Ken

> -----Original Message-----
> From: [hidden email]
> [mailto:[hidden email]] On Behalf Of Jochen Fromm
> Sent: Thursday, November 06, 2008 11:35 PM
> To: The Friday Morning Applied Complexity Coffee Group
> Subject: Re: [FRIAM] AMS Notices: A Special Issue on Formal Proof
>
> nice quote
>
> > "Is current mathematical notation today's roman numerals, a
> syntax we
> > have to leave behind or enhance to integrate with algorithms or
> > "scripts""
>  
>
> -J.
>
> ============================================================
> FRIAM Applied Complexity Group listserv
> Meets Fridays 9a-11:30 at cafe at St. John's College
> lectures, archives, unsubscribe, maps at http://www.friam.org


============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
lectures, archives, unsubscribe, maps at http://www.friam.org