leancrawler bug

Stream: condensed mathematics

[Riccardo Brasca]

CC @Patrick Massot

[Patrick Massot]

Thanks for creating an easy case. I will investigate this but time is currently a very very scarce resource for me.

[Patrick Massot]

I'll try anyway at some point in the near future since it could be useful for our project paper writing

[Johan Commelin]

@Riccardo Brasca Thanks for minimizing!

[Riccardo Brasca]

I am opening a separate discussion, maybe someone else is interested in this.

[Patrick Massot]

Wait, I don't understand the complain. Your example mentions crawler.comm.comm whose dependencies should mention nat.add_comm

[Riccardo Brasca]

That is my complain, I don't see anywhere nat.add_comm

[Patrick Massot]

What you are printing here are only the direct dependencies, you need the full graph to see transitive dependencies

[Patrick Massot]

What does it says about test?

[Riccardo Brasca]

In [3]: lib['crawler.test']

Out[3]: LeanDecl(name='crawler.test', filename='/home/brasca/lean/test_crawl/src/test_crawl.lean', line_nb=10, kind='definition',
is_inductive=False, is_structure=False, is_structure_field=False, is_class=False, is_instance=False, is_recursor=False,
is_constructor=False, Type='crawler.comm', type_uses_proofs=set(), type_uses_others={'crawler.comm'}, type_size=0,
type_dedup_size=0, type_pp_size=0, Value='{x := 2, y := 5, comm := crawler.test._proof_1}',
value_uses_proofs={'crawler.test._proof_1'}, value_uses_others={'nat.has_add', 'bit1', 'nat.has_one', 'bit0', 'crawler.comm.mk',
'nat', 'has_one.one'}, value_size=0, value_dedup_size=0, value_pp_size=0, target_class=None, parent=None, fields=[])

[Johan Commelin]

Ok, and for crawler.test._proof_1?

[Riccardo Brasca]

it's not happy.

[Riccardo Brasca]

Meaning it gives an error

[Johan Commelin]

So maybe that's the issue? Because I guess that is where nat.add_comm is supposed to show up.

[Riccardo Brasca]

nat.add_comm is indeed present in the full graph, but not in the connected component of crwaler.stupid. Maybe I don't understand something, but it should show up, right?

[Riccardo Brasca]

I mean, it is needed

[Johan Commelin]

Right, so somehow the code fails to add an edge. And it might be related to the fact that you got an error when querying about ._proof_1?

[Riccardo Brasca]

I think the error is there, but I have no idea how the script works. In any case

nx.shortest_path(G, 'nat.add_comm', 'crawler.stupid')

gives

...
NetworkXNoPath: No path between nat.add_comm and crawler.stupid

[Patrick Massot]

Ok, there is a clear bug here. Floris and I will try to fix it soon.

[Patrick Massot]

Thanks for you help!

[Riccardo Brasca]

The full graph has 5177 nodes. To prove that 2+3=3+2. Crazy.

[Kevin Buzzard]

Lean has proved that math is hard!

[Mario Carneiro]

to be fair, there is a proof of 2+3=3+2 that involves only eq.refl, nat.zero and nat.succ

[Riccardo Brasca]

Maybe this is because I used structure. In any case it is not so important.

[Riccardo Brasca]

And it is the full set of declarations used in init.data.nat.lemmas I think.

[Floris van Doorn]

This should be fixed in leancrawler#7.
You can already test this by manually changing your crawl.lean file.

[Johan Commelin]

Cool! Thanks for hacking on this! Should Riccardo's MWE be recorded as a test in the repo?

[Johan Commelin]

@Riccardo Brasca Can you now calculate how many definitions go into LTE? (As opposed to lemmas.)

[Johan Commelin]

Maybe I actually want to know this for the statement, instead of the entire proof.

[Johan Commelin]

I guess we should prepare a def statement : Prop := ... to do that.

[Riccardo Brasca]

Yes I am going to run it against the LTE to gather the stats as before

[Riccardo Brasca]

But you'll have to wait until this afternoon for the results I think

[Riccardo Brasca]

@Johan Commelin do you like this statement?

def liquid_tensor_experiment_statement (S : Profinite.{0}) (V : pBanach.{0} p) : Prop :=
  ∀ i > 0, is_zero (Ext i (ℳ_{p'} S) V)

[Johan Commelin]

@Riccardo Brasca LGTM

[Johan Commelin]

You could just copy the statement from challenge.lean

[Johan Commelin]

I think it uses \iso 0, instead of is_zero.

[Johan Commelin]

But that shouldn't really have any effect on the nr of defs used in the statement.