I don't want to formalize any of my work on mathematics.

[robjlow@mathstodon.xyz]

@dpiponi @johncarlosbaez I managed to get as far as a DPhil without any formal (sorry) education in the foundations of maths. The only times I recall it rearing its head were the passing comments in topology that Tychonoff's theorem needed the axiom of choice, and likewise in measure theory for non-measurable sets.

[sjb@mstdn.io]

@johncarlosbaez @andrejbauer You don't have to think in the formally correct way, but it helps to know what the formally correct way is.

[thebluewizard@masto.hackers.town]

@mevenlennonbertrand @MartinEscardo I have developed stuff using C language for many years. The thing is, it requires a good understanding of the C in order to properly program stuff. C is notorious for many UBs (undefined behaviors), for lax typing, etc. And it requires more coding and debugging to achieve things. This is one reason why many other languages such as Python are used. I myself use Python instead of C for quick programming (zero worry about memory leak or corruption). Just FYI.

[johncarlosbaez@mathstodon.xyz]

@RobJLow @dpiponi - I spent a huge amount of time learning logic, computability theory, and set theory as a kid, then got sick of that because it seemed the rest involved large cardinals and forcing, which didn't appeal to me. So around 1982 I quit thinking about this stuff. By the time I heard about the exciting newer approaches to logic, like topos theory and type theory, I was much less engrossed and picked it up slowly except for the categorical approach to quantum logic. Then homotopy type theory was born... right around when I'd lost interest in homotopy theory.

[chrisamaphone@hci.social]

@pigworker @andrejbauer @xenaproject @JacquesC2 @MartinEscardo @johncarlosbaez @dougmerritt btw, in light of this discussion, you folks might be interested in this work: https://hci.social/@chrisamaphone/116324984760765758

[oantolin@mathstodon.xyz]

@sjb I think the point that both @johncarlosbaez and @andrejbauer are making is that there is no single correct to way to think, whether you are working formally or traditionally.

[refurioanachro@mathstodon.xyz]

Have a look at these Lean games:

Lean Game Server

(adam.math.hhu.de)

It's good to work a few examples to see how they spell out in a proof assistant. It's not difficult! It's fun!

I see proof assistants as a sort of calculator for assumptions. They really shine when you throw lots of stuff at them, like verifying computer programs. Which involves lots of boring stuff, and a proof assistant can help with that! If it's a burden then don't use a proof assistant.

@johncarlosbaez @MartinEscardo

[refurioanachro@mathstodon.xyz]

@johncarlosbaez asked:
> how long would it take?

I just noticed I didn't answer your question. An hour is fine. More is more.

@MartinEscardo

[martinescardo@mathstodon.xyz]

@johncarlosbaez It is absolutely fine not wanting to try it.

But then please stop saying things such as "I don't think formalizing mathematics at all makes us think the right way" or other claims about formalization.

If you want to speak with authority about formalization, then learn it first. And, yes, it is not easy or fast to learn it.

[yinyangmills@mathstodon.xyz]

@markusde @JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker Ok, so what is better (ie worse) than Lean?

[mc@mathstodon.xyz]

@ohad @JacquesC2 @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject yeah but that's not my point. is formal-first, agda-as-a-blackoboard, a good fit for those disciplines with the current tools? one can definitely argue for formalization of the results *at some point* as a means to check their correctness (I'm a bit skeptical of that too, but it's not a hill I want to die on)

[mc@mathstodon.xyz]

@andrejbauer @JacquesC2 @cbaberle @johncarlosbaez @dougmerritt @MartinEscardo @pigworker @xenaproject what do you mean? (for the record, *I* am not blaming anyone for anything)

[jacquesc2@types.pl]

@mc
As a rule of thumb, I'd say if a domain has had 5+ formalizations already, then yes, formal-first works. Two or less, likely not.

My 5 might be too low.

@ohad @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject

[dearlove@mathstodon.xyz]

@andrejbauer @johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject And as well as those working at the cutting edge, we want mathematicians working on more mundane matters. Playing with simple (especially by cutting edge standards) probability and statistics matters, I see and use some things that didn't exist when I was an undergraduate. For example, estimating the confidence interval of a binomial probability, methods have got better.

[ohad@mathstodon.xyz]

@JacquesC2 I haven't got to the point where I can use a tool like Agda the way I use a whiteboard for my own research the way Martín uses it.

I have used it as a whiteboard to explain concepts to other people, but that's probably because we insist on clipping our students' wings by not teaching them the relevant mathematics.

I say 'students' here with a very broad interpretation, we are all students indefinitely.

@mc @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject

[martinescardo@mathstodon.xyz]

@mc

You don't need to formalize all prior art to be able to do what you want in blackboard mode.

For example, @de_Jong_Tom and I used a result by Mike Shulman, which was published and also formalized in Rocq/HoTT, in TypeTopology.

We didn't want to formalize it (although I have been entertaining the possibility of formalizing it, to understand it better, in my own terms - formalizing for the sake of thinking about it).

So we just used it as a hypothesis to our desired result. That is, we proved "Shulman's result implies our result".

This doesn't establish the ultimate truth of our result in TypeTopology.

But it does allow us to keep using TypeTopology as a blackboard, without worrying about formalizing everything that every mathematician has done in this planet in order to carry on.

And without any lack of honesty. All assumptions are explicitly given. The adopted `--safe` flag guarantees that. There are no postulates. Just explicit assumptions.

@ohad @JacquesC2 @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @pigworker @xenaproject

[ohad@mathstodon.xyz]

@JacquesC2 that said, I typically don't use tools like Agda to check my maths anyway. Rather, I do some maths (traditionally, on the whiteboard, then on paper, then in LaTeX) in order to work out how to explain enough of it to Agda or Idris so it will let me write a program I cannot write in other kinds of languages.

@mc @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject

[tobybartels@mathstodon.xyz]

@MartinEscardo @andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject

It seems to me that anything that translates careful but informal mathematical vernacular into a formal language, must ipso facto be AI. But that doesn't mean that it would be the kind of AI that you describe as unhelpful at the end of your post. Rather, it means that AI encompasses much more than those things.

[martinescardo@mathstodon.xyz]

@ohad writes "we are all students indefinitely."

+∞

I certainly am. Of mathematics and everything.

@JacquesC2 @mc @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @pigworker @xenaproject

[martinescardo@mathstodon.xyz]

@TobyBartels It is interesting you say this.

Some things that were considered AI in the past are now deterministic algorithms.

For example, checking formal proofs with incomplete information (to be reconstructed by the checker) for correctness.

@andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject