Xena Project

> In any case, to my knowledge, no cipher has ever unconditionally been proven secure except the one time pad.

Essentially yes.

> We just have a bunch of conditional security proof that are correct if the underlying assumptions (e.g. factoring primes is hard) are correct.

Again correct.

regarding Wiles proof of FLT: you may enjoy reading:

https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/

I understand you for now lack the information I possess, but from my perspective I can absolutely confirm that FLT is correct, since I have a concise proof of it, which even interested highschoolers would be able to follow.

Even in a world where multiple formalized proofs will exist: who's opinion on the security of modern cryptographic protocols would you be more willing to follow:

those cryptographers who fail to prove FLT on their own, which is 99.999% of cryptographers today

a group of mathematicians that together painstakingly formalize a huge detour to prove it,

or a person who proved FLT on their own, thereby proving Fermat could have done the same, in stark contrast to Wiles who argues that Fermat couldn't have possessed such a proof "since not enough mathematics had developed yet in his era in order to prove it" so to speak?

suppose you find yourself lost in the streets of Tokyo, and ask a Prophessor of Geography how to get to destination X and someone who overhears the conversation the same? The person who overheard the conversation claims…

TIL: Fields medallists ask questions on MathOverflow... [1]

This has me in awe about the depth of mathematics, the pace of progress, the miracle of specialisation. I have a degree in an applied-math-y adjacent field, and understand nothing. (And, btw, I was astonished how knowledgable some commenters right here were, and then realised that we have the (co-)authors of the results themselves here! gotta love HN.)

With that said, here some (non-mathematical) snippets I found interesting (apart from the great word "sheafification"):

> Why do I want a formalization?

> — I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. In the end, we were able to get an argument pinned down on paper, but I think nobody else has dared to look at the details of this, and so I still have some small lingering doubts.

> — while I was very happy to see many study groups on condensed mathematics throughout the world, to my knowledge all of them have stopped short of this proof. (Yes, this proof is not much fun…)

> — I have occasionally been able to be very persuasive even with wrong arguments. (Fun fact: In the selection exams for the international math olympiad, twice I got full points for a wrong solution. Later, I once had a full proof of the weight-monodromy conjecture that passed the judgment of some top mathematicians, but then it turned out to contain a fatal mistake.)

> — I think this may be my most important theorem to date. (It does not really…

> The FOM folk are in general incredibly bearish on proof assistants, so of course they don't care. If you only care about an 'ultimate' foundation that is the best fit to evaluate other systems, rather than a foundation that is amenable to actively working with it, of course you have no reason to care about HoTT.

> If you share their opinion, alright, but I personally find this incredibly myopic.

I want to distinguish between two senses of "foundation of mathematics":

1) An ontologically minimal language to formalize mathematical reasoning and facilitate proving things about (in)consistency, provability, and relative theory strength, and generally doing metamathematics.

2) A language to actually carry out the details of formalizing mathematics, perhaps jointly by humans and computers, in the sense of the Xena Project and proof assistants.

Here is a claim which might annoy you, but really ought to be uncontroversial: the correct meaning of the term "foundation of mathematics" is the first one. This is what it has meant for about a hundred years, at least, and what someone working professionally in the reverse mathematics/set theory/model theory/logic communities will understand the phrase to mean if you use it in conversation with them.

Now, given this, and given you agree that ZFC does a better job at function (1) above, I think this explains why the FOM people (and more generally those in the communities I listed) find it strange when HoTT is suggested as a…

> I feel like a proof assistant is amongst the worst places to have something like this

It's one of the best places! You know how in programming, your code looks like this?

func my_function(inputs) -> output
{ do something }

In theorem proving, it's almost the same:

theorem my_theorem(assumptions) -> conclusion
{ prove something }

But there's a single crucial difference: in programming, the "do something" is really important, whereas in Lean, the "prove something" isn't important at all: as long as the typechecker is happy with it, everyone can forget about it once it's written.

So as long as your assumptions and conclusion don't involve any division by zero, it doesn't matter what goes on inside the proof.

Regarding division by zero, you sort of have three options:

* Output an error / checked null when there's division by zero.

* Require a proof that the denominator is nonzero before you're even allowed to use division.

* Allow division by zero, making it return some nonsense. Then, add an assumption that the denominator is nonzero to all your theorems about division.

The first two options (especially the second one) make the definition of functions that involve division horrifically messy. (Idk, it might be easier if Lean had exceptions, but that also sounds messy.) I think that's why Lean goes with the third option.

https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

I think the same problems manifest in math, but to a different degree and in a different way. We do have some expectation of universal mathematics literacy, or at least math is a required subject in most schools around the world.

But I don't think that math education is generally very successful at teaching people math, as described in Lockhart's Lament: https://www.maa.org/sites/default/files/pdf/devlin/LockhartsLament.pdf

My suspicion is that a big part of the issue is the way math is presented early on is really tedious and boring to a lot of people, in a way that could be addressed by theorem provers. I think something like the Xena Project https://xenaproject.wordpress.com/what-is-the-xena-project/ is potentially an interesting development in that regard (though more for undergraduate math than grade school math).

I also don't think this is anyone's "fault" really. I'm more interested in figuring out what might make things better than assigning blame. Nor do I think I personally can fix it single-handedly with a new programming language. If Yatima can move the ball forward a little bit by eventually contributing to a few people learning and falling in love with programming and math, that's more than enough for me.

Computers can and should help along the way, but Dijkstra's argument is that a) much of the challenge of human ideas is discovered in the act of converting from natural to formal language and b) that this act, in and of itself, is what trains our formal logical selves.

So he's contesting not only the idea that programs should be specified in natural language, but also the idea that removing our need to understand the formal language would increase our ability to build complex systems.

It's worth noting that much of the "translation" is not translation, but fixing the logical ambiguities, inconsistencies and improper assumptions. Much of it can happen in natural language, if we take Dijkstra seriously, precisely because programmers at the table who have spent their lives formalizing.

There are other professions which require significant formal thinking, such as math. But also, the conversion of old proofs into computer proofs has lead us to discover holes and gaps in many well accepted proofs. Not that much has been overturned, but we still do t have a complete proof for Fermats last theorem [1].

[1] https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/