Context-free pumping lemma

Stream: general

[Martin Dvořák]

This is a long shot but ... would anyone like to prove the Pumping lemma for context-free languages?
Statement:
https://github.com/madvorak/grammars/blob/main/src/context_free/cfgPumping.lean

I think it might be a good topic for a bachelor thesis or something. There already exists a proof in Coq.

[Kevin Buzzard]

Why don't you find an undergraduate at your university and supervise them through it?

[Martin Dvořák]

Because there are no undergraduates at my university.

[Pedro Sánchez Terraf]

Martin Dvořák said:

This is a long shot but ... would anyone like to prove the Pumping lemma for context-free languages?

I assume that the Pumping Lemma for regular languages is already there... Is Kleene theorem already formalized?

[Martin Dvořák]

Pedro Sánchez Terraf said:

I assume that the Pumping Lemma for regular languages is already there.

https://github.com/leanprover-community/mathlib/blob/c34a1aa4263bdf585dd705508c11d3b75836049e/src/computability/DFA.lean#L126

[Martin Dvořák]

Pedro Sánchez Terraf said:

Is Kleene theorem already formalized?

Not yet afaik.
https://github.com/leanprover-community/mathlib/blob/2ce8482e27326fdbbc45324102cd03056e556b80/src/computability/regular_expressions.lean#L18