resources.html

---
layout: page
title: Resources
description:
background: '/img/maths_background.png'
mathjax: true
---

<style> 
  nav a{text-decoration: none;}
  
  a.item-link{text-decoration:underline;}
  
  #goals > ol > li> a
    {
     text-decoration:underline;
    }
  
<!--   goals > p > ol > li a{
text-decoration: underline;
  } -->

</style>  

<h3 class="section-heading">Project Overview</h3>

<p> <a href="https://gowers.wordpress.com/2022/04/28/announcing-an-automatic-theorem-proving-project">An announcement of the project</a>.</p>

<p> <a href="https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view">A more detailed document about it</a>.</p>

<p> <a href="{{site.baseurl}}/2022/09/09/basicalgorithm.html">A blog post explaining some of the basic problem-solving moves</a>.</p>

<h2 class="section-heading">Minutes</h2>

<p> An <a href="{{site.baseurl}}/minutes.html">informal record</a> of meetings of participants based in Cambridge. </p>

<!-- <p> An <a href="{{site.baseurl}}/2022/09/09/subtasks.html">testing</a> blog.</p>
<p> An <a href="{{site.baseurl}}/2022/09/09/basicalgorithm.html">testing</a> blog.</p> -->

<h3 class="section-heading">Examples of the proof discovery process</h3>

<p> We are trying to formulate a notion of "motivated proof". Roughly speaking, this means a proof that does not involve rabbits being drawn out of hats. While we do not yet have a precise notion yet, <a href="{{site.baseurl}}/motivatedproofexamples.html">we do have several examples</a>. </p>

<p> Two YouTube series of live problem-solving videos have been created by Tim Gowers. One focuses on <a href="https://www.youtube.com/playlist?list=PLOft35kj95aajgXAFHKklygbpsESMQUid">problems that require the solver to find useful invariants</a>, while the other is for <a href="https://www.youtube.com/playlist?list=PLOft35kj95aYGeaJQlD8NSroMlWfkiJ1F">problems that require clever colourings</a>. We would be delighted to link to similar videos made by others (of any kind of non-routine problem -- they don't have to be IMO-style problems): please let us know of any that you know of, or have made yourself. To be useful for this project they should be of people solving problems they have not seen before, rather than merely explaining solutions they know.</p>

<h3 class="section-heading">A list of challenge problems</h3>

<p> The problems that we are trying to solve are a little different in style from the benchmark problems one finds in typical databases, in that they are more like the easier problems that one might find in a mathematics undergraduate problem set. So we would like to create our own collection of problems and use it to measure our progress. We have made <a href="{{site.baseurl}}/problemlist.html">a start on this</a> and would welcome further suggestions. </p>

<h3 class ="section-heading">A large number of previously private blog posts</h3>

<p> For several years, Mohan Ganesalingam and Timothy Gowers collaborated using a private blog. <a href="https://robotmaths.wordpress.com/">The content of that blog is now publicly accessible</a>. There are a lot of posts, and many of the ideas they contain are fairly half baked, or superseded by later ideas that seem to work better. But a lot of them also represent trains of thought that were not fully explored and could be a useful starting point for further research.</p>