Alex Kontorovich - Rough Structure and Classification, Revisited

See Tim Gowers' publications list https://www.dpmms.cam.ac.uk/~wtg10/papers.html where you can get a PostScript copy of this 200 paper:

This was my attempt to do the `Hilbert thing', at a conference in Tel Aviv in 1999 entitled Visions in Mathematics . I start with some speculations about computers - I think that before too long they will have a much more serious role to play in helping mathematicians to find proofs, or even finding proofs for themselves. I then make some general remarks about what I call `rough structure' and `rough classification' in combinatorics, stating several problems that I find interesting. In a final section, I give a more miscellaneous list of (mostly well known) open problems that I would love to see solved. Unlike Hilbert, I do not intend my list of problems to have a major influence on the course of mathematics in the next century - it is just a list of problems that I like.  See Tim Gowers Talking About Human-Oriented Automated Theorem Proving.

He's going to try teaching some hgh-school students in New Jersey to formalise book I of Euclid's Elements using Jeremy Avigad's A Formal System for Euclid's Elements. See https://github.com/ah1112/synthetic_euclid_4, and this podcast with André Hernández-Espiet.

42:49 He's quite explicitly looking at this as a way to feed Alpha Proof with human input. And on the business with LaTeX/TeX maintaining itself from now on, using AI. Well, let's wait and see. I don't think he has even a faint clue what is going on underneath systems like Overleaf.
 

Subscribe to INI.

Comments

Post a Comment

Popular posts from this blog

How Could One Unify CMU and MIT

Image
I mean, how to get the best of the two different philosophies of computation. One is based on typed programming languages and the other on engineering with diagrams . This is about practical computing and the cost and feasibility of software development in general. Here is the problem: We have a lot of algorithms which can all be described abstractly using some sort of pseudocode, or perhaps using some particular language (usually Python!). These algorithms are often well-studied and a lot is known about them in terms of their computational complexity in time and space. Substantive practical software systems invariably employ many such algorithms, often implemented in libraries with more or less well-specified APIs. But very few of these libraries are capable of interoperating because they are either packages written in some specific programming language like Java or Haskell, say, or they are written in C and used as object code, or they are written in an interpreted language like Sc...
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

HTML in Blog Posts

Just testing stuff: SVG You can click on the blue circle: MathML There is not much you can do with this. See Mathematical Markup Language 1.01 Specification   7.1.5 Mixing and Linking MathML and HTML . It's the big problem  of how you compose languages.   a x 2 + b x + c = 0 You can click on the discriminant: x = − b ± b 2 − 4 ⁢ a ⁢ c 2 ⁢ a 2D Canvas Sound  Beep! WebGPU Next level Parser expression grammar compiler:  https://peggyjs.org/online.html Devine Lu Linvega's unxtal assembler/debugger:  https://wiki.xxi...
Read more