Quanta article

Stream: general

[Jeremy Avigad]

A nice article about the use of SAT solvers to resolve the Keller conjecture: https://www.quantamagazine.org/computer-search-settles-90-year-old-math-problem-20200819.

[Jesse Michael Han]

interestingly, Tom and not Marijn is quoted on SAT solving basics

“You just decide whether each variable is true or false in a way to make the whole formula true, and if you can do it the formula is satisfiable, and if you can’t the formula is unsatisfiable,” said Thomas Hales of the University of Pittsburgh.

[Shing Tak Lam]

New Quanta article on ATP/ITPs

https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/

[Bryan Gin-ge Chen]

Sadly, Lean isn't mentioned (explicitly, at least).

[Kevin Buzzard]

There's another one in a couple of weeks which will

[Scott Morrison]

This one is actually pretty good!

[Scott Morrison]

even if it doesn't satisfy our partisan fantasies

[Patrick Massot]

It seems they want a lot of papers about computerized maths. Hartnett wrote https://www.quantamagazine.org/can-computers-solve-the-collatz-conjecture-20200826/ and https://www.quantamagazine.org/computer-search-settles-90-year-old-math-problem-20200819/ about ATP and we know he works on something about ITP, and now we have this paper which is about both.

[Stanislas Polu]

Let's hope that we'll get them excited as we apply GPT (at scale) to Lean :)

[Johan Commelin]

Response by Harris: https://mathematicswithoutapologies.wordpress.com/2020/09/01/the-inevitable-questions-about-automated-theorem-proving/

[Mario Carneiro]

His objections don't really make sense to me. I gather that he feels slighted by the journalistic spin, but the source of his disapproval seems to be some anti-capitalist thing. I feel like he needs to spell out his doomsday scenario more precisely for his concerns to come across better

[Anne Baanen]

I understand it as three related points. First, Harris wants to point out that there are questions worth asking that are not asked by the usual journalistic approach to AI. That is, an article can ask: "will/does this AI that is being developed solve a specific goal?" and "if this AI can solve a specific goal, will that be good or bad?", but not "how do we choose the goals that we develop AI for?", and "how do we choose what good and bad mean?" and most importantly "who is this 'we' that gets to choose?".

Secondly, when Harris tries to raise these questions, they get eroded away as articles are redrafted because these questions do not fit into the typical paradigm.

And the remainder of the post argues the answers to the unasked questions are often "a goal is chosen iff solving it means profit", "good means that the US economy scores better on some measurement" and "big companies control how they invest their money, so they choose which projects get funded". The article states that you can decide whether these answers are concerning, and implies they are in Harris's opinion.

[Mario Carneiro]

I still don't see how businesses doing business things using math at all represents a threat to mathematicians that do it "for fun" / pursuing their own goals. That is, I challenge the "iff" in the first answer, unless by "a goal is chosen" you mean "a goal is chosen by big companies"

[Mario Carneiro]

in fact, I dare say it's a good thing because mathematicians like us often subsist on the scraps left from funding by big businesses with big business goals, to do our own projects

[Mario Carneiro]

lean itself wouldn't exist if it wasn't for the fact that leo had enough discretionary funding to work on a theorem prover for microsoft

[Ruben Van de Velde]

I suppose one question that might be asked is - could we imagine a world where mathematicians don't have to subsist on those scraps

[Reid Barton]

That's how pretty much all pure math research has operated for the past 100+ years.

[Scott Morrison]

Built the bomb? Cracked enigma? Sure, stick around, we'll find something for you to do.

[Reid Barton]

All I'm saying is that when somebody decided to, say, characterize which topological spaces are the underlying spaces of schemes, that problem wasn't selected for the purpose of maximizing the click-through rate on ads.

[Mario Carneiro]

Ruben Van de Velde said:

I suppose one question that might be asked is - could we imagine a world where mathematicians don't have to subsist on those scraps

I don't think this will ever happen unless we reach a post-scarcity economy, because mathematics isn't "useful", it is useful-adjacent

[Kevin Buzzard]

Several of my former PhD students have, after having been trained by me, disappeared off into GCHQ...

[Scott Morrison]

The impressive thing is that a bunch of people discovered how to carve out a post-scarcity world, where they could think about underlying spaces of schemes, as a bubble, more or less, embedded in the world that Vannevar Bush, etc., built.

[Jeremy Avigad]

https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/
Lovely!

[Jasmin Blanchette]

I'm sure Larry Paulson will be thrilled about all the references to Alexandria.

[Kevin Buzzard]

I was sent a draft of the "anatomy" diagram and they had used N instead of \N. Because @James Arthur once told me that the reason he thought Lean was cool was because of the bold face font, I quickly suggested to Kevin Hartnett that he change it!

Thrilled to see @Heather Macbeth and @Amelia Livingston mentioned.

[Kevin Buzzard]

Did I also see a PR changing fact to factorial today? Was that so that the mock-up code typechecked?

[Heather Macbeth]

The photo of @Kevin Buzzard's office makes me feel better about the fire hazard in mine!

[Kevin Buzzard]

it's what maths looked like in the old days

[James Arthur]

Kevin Buzzard said:

I was sent a draft of the "anatomy" diagram and they had used N instead of \N. Because James Arthur once told me that the reason he thought Lean was cool was because of the bold face font, I quickly suggested to Kevin Hartnett that he change it!

Thrilled to see Heather Macbeth and Amelia Livingston mentioned.

Wooo! My little influence made an N into an \N!

[Patrick Massot]

Jasmin Blanchette said:

I'm sure Larry Paulson will be thrilled about all the references to Alexandria.

I'm pretty sure Hartnett came up with this on its own. Nobody here ever uses this reference.

[Patrick Massot]

And it's true that Isabelle isn't mentioned much.

[Patrick Massot]

It also sounds like Zulip is only this instance, and this is probably our fault since we indeed use the word Zulip to mean this server in particular.

[Rob Lewis]

Hah, I've wondered how big our Zulip instance is compared to others. Big enough to be called out on their website: https://zulip.com/for/research/

[Mario Carneiro]

I think the Rust zulip is quite a bit bigger than ours, and possibly the other big programming languages might also have decent turnout, but I don't think there are too many

[Patrick Massot]

I'm happy to see my suggestion to watch Scott's intro to LFTCM video was very successful.

[Johan Commelin]

Yes, I think that's one of the best things that could have happened. (-;

[Johan Commelin]

Let's hope those recordings will be useful in the next couple of days (-;

[Arthur Paulino]

Quanta article about Leslie Lamport:
How to Write Software With Mathematical Perfection

[Julian Berman]

In the video he makes a passing comment about a scenario in TLA+ where after writing a proof he realized there was an unused hypothesis that he was able to delete, which probably resonates with folks from similar situations in mathlib :)

[Kevin Buzzard]

I'm currently watching Patrick's IAS video and he also gives an example of this issue .

[Yakov Pechersky]

It's too bad that the sounds cuts out for the last portion of that video