Emily Riehl - Formalizing invisible mathematics: case studies from higher category theory

This was given on 9th June and has been reuploaded:

 

See this MathOverflow discussion with the response by Andrej Bauer: What makes dependent type theory more suitable than set theory for proof assistants? and Andrej Bauer's "Five Stages of Accepting Constructive Mathematics".

See Tim Gowers Talking About Human-Oriented Automated Theorem Proving.

Ursula Martin's talk "Will machines change mathematics?" part of a workshop Modern History of Mathematics: Looking Ahead.

18:48 Max Newman's 1946 Royal Society Grant Proposal: see Simon Lavington's Early Days of Computing at Manchester: Max Newman's Royal Society Project, 1946–1951:

Max Newman became Professor of Pure Mathematics at Manchester University in 1945, having led the outstandingly successful Colossus cryptanalytical project at Bletchley Park during the war. He obtained Royal Society funding to set up a Computing Machine Laboratory at Manchester to apply similar digital electronic technologies to the solution of as-yet unsolved problems in pure mathematics. But what kind of (special-purpose) digital computer was likely to be most suitable? Using new evidence, this article charts the progress of Newman's project in some detail, attempting for the first time to set Newman's Colossus-centric vision in the context of John von Neumann's IAS architecture. We contrast mathematical and engineering perspectives. Though Max Newman's original plans were not realized, innovative computer design at Manchester flourished in directions unforeseen by Newman. It was his 1946 initiative that led, somewhat indirectly, to significant computing milestones. 

For more on Newman's influence on type theory, see David MacQueen's remarks in Numberphile - Sophie Maclean on the Catalan Numbers.

Ekaterina Babintseva - Freedom and control: pedagogical computing in the US and the Soviet Union:

In the mid-twentieth century, the United States and the Soviet Union came to believe that the future of each country hinged on capable technoscientific workforce. To cultivate such workforce, researchers in both countries suggested replacing human instructors with special pedagogical computers to turn learning and teaching into an effective and fully controllable process.  At the same time, in the 1960s and the 1970s, both American and Soviet societies saw the rising urgency of the concept of creativity. This presentation explores how researchers in each country navigated the challenge of turning the mid-century computer, a paradigmatic command and control machine, into the technology that could cultivate creative thinking. In doing so, this talk explores the historical intersections of human sciences and computing, treating pedagogical computing as an effort in engineering human behavior and thinking. 

That last sentence reminds me of the slightly queasy feeling I got when I saw a set of "scratch coding cards" in the Raspberry Pi shop in Cambridge the other day. The thought that thousands of children were being taught to analyse computational structure solely in terms of Von Neumann machines, and not as recursive structures, gives me the creeps.

 

Subscribe to INI

Comments

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Welsh Republic Podcast Talking With Kars Collective on Armenia Azerbaijan Conflict

Hitachi HD44780U LCD Display Fonts