salamander tactic

Stream: condensed mathematics

[Johan Commelin]

I'm posting a stub here. Please reply if you are interested in working on the salamander tactic. We'll need people with expertise in

1. the widget framework
2. tactic writing
3. diagram chasing

[Riccardo Brasca]

I am interested. I know essentially nothing about tactic writing, but this is a good opportunity to learn.

[Alex J. Best]

I'm interested too :smile:!

[Johan Commelin]

What I figured out is that if you put together some of the basic construction that go into this Salamander lemma, there is at most 1 morphism that you can construct between any two objects in the double complex (up to propositional equality).

[Johan Commelin]

Somehow, we should capitalize on that fact, because it means that when you are inside "salamander mode" you basically don't care about morphisms (beyond their existence).

[Yaël Dillies]

You're using your funding to build a game, and I know it! :stuck_out_tongue_closed_eyes:

[Eric Rodriguez]

One thing I do wonder is how good of an idea it is to build this in Lean3, instead of waiting for Lean4 which (should?) have better support for this sort of thing

[Johan Commelin]

I think we can already explore a bunch of ideas in Lean 3

[Johan Commelin]

But we should certainly keep an early switch to Lean 4 in mind. Especially if LTE will not depend on this.

[Adam Topaz]

Johan Commelin said:

Please reply if you are interested in working on the salamander tactic...

Count me in. I also know very little about tactic writing.