I don't want to formalize any of my work on mathematics.
-
@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
@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
-
@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)
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
-
@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
@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
-
@andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
It is not inconceivable that one day in the not-too-distant future, proof assistants will be able to "understand" proofs written in sufficiently careful, informal, mathematical vernacular and translate it to a suitable formal language.
And this formal language doesn't need to be fixed. The mathematician just chooses a foundation, or, in case they don't care, they let the proof assistant choose a suitable one for the informal (but hopefully rigorous) mathematics at hand.
I don't mean AI, but people are certainly trying this with so-called AI nowadays (personally, I think this is the wrong approach, but **I don't want** this to become the subject of discussion here).
In any case, a person will need to check that the definitions and the statements of the theorems and constructions are correctly translated (*). Then the formal proofs obtained from informal proofs don't need to be checked by people.
(*) At least at the beginning. For example, we now trust that C compilers produce correct machine code and don't check it ourselves.
In any case, all of the above can happen only step by step, and currently we are at an important step, I think, where the first were in the 1960's by de Bruijn.
As I said before, I use proof assistants as smart blackboards. If I could get interactive help while I write in mathematical vernacular, I would immediately adopt this incredible new proof assistant.
And, I repeat, I don't mean the kind of non-help I get from ChatGPT, Gemini, Claude, DeepSeek, or what-you-have - I feel I help them rather than the other way round.
I mean the kind of help I already get in non-AI-based proof assistants
@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.
-
@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
@ohad writes "we are all students indefinitely."
+∞
I certainly am. Of mathematics and everything.
@JacquesC2 @mc @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @pigworker @xenaproject
-
@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.
@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
-
R relay@relay.mycrowd.ca shared this topic
