Pfaffians?

Stream: maths

[Darij Grinberg]

Does Mathlib know about Pfaffians? perfect matchings of [2n] and their enumeration? what is the easiest way to find out?

[Riccardo Brasca]

"pfaffian" does not appear anywhere in mathlib (nor in the code nor in docstrings) so the answer is probably that we don't have anything about it.

[Bryan Wang]

Darij Grinberg said:

what is the easiest way to find out?

I usually start with https://leanprover-community.github.io/mathlib-overview.html, though this is not always most updated (but the links there bring you to the docs, which are updated)

[Darij Grinberg]

@Bryan Wang thanks, but I'm not sure where to look for this... logically should be in linear algebra but could be wherever it is used

[Darij Grinberg]

thanks @Riccardo Brasca

[Adrian Marti]

I also tried searching with leanexplore, which also returned no hits.

[Bryan Wang]

but as of now the easiest way is usually to ask here :rolling_on_the_floor_laughing:

[Darij Grinberg]

thanks @Adrian Marti !
i feel like i should also have the source somewhere on my computer to grep, but i have no idea where VS Code has put it :blushing:

[Kenny Lau]

github has a search feature already, https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4%20pfaffian&type=code

[Darij Grinberg]

oooh nice

[Bryan Wang]

Darij Grinberg said:

Bryan Wang thanks, but I'm not sure where to look for this... logically should be in linear algebra but could be wherever it is used

There's also a section on enumerative combinatorics further down

[Kenny Lau]

loogle also has search by string feature, https://loogle.lean-lang.org/?q=%22pfaff%22

[Kenny Lau]

in contrast with leanexplore, loogle does not use LLM

[Adrian Marti]

I struggle with effectively using loogle, but that's probably because I don't really understand how to use it :joy: :joy:

[Kenny Lau]

@Adrian Marti it matches either parts of the statement or parts of the name of the theorem

[Kenny Lau]

for example if you know that a theorem talks about the Nat.card of something then you can use Nat.card as one of the search inputs

[Kenny Lau]

the inputs are separated by commas

[Kenny Lau]

e.g. if you want to find all theorems that talk about when a cosine is zero, you would do Real.cos _ = 0

[Kenny Lau]

https://loogle.lean-lang.org/?q=Real.cos+_+%3D+0

[Adrian Marti]

So let's say I want to extend a function Fin n -> X to a function Fin (n + 1) -> X given an a: X. Can I search this with loogle?

[Darij Grinberg]

i don't get loogle either, but searching for a word is probably the easiest way of using it :)

[Riccardo Brasca]

Adrian Marti said:

So let's say I want to extend a function Fin n -> X to a function Fin (n + 1) -> X given an a: X. Can I search this with loogle?

You can see if there is a literal way of doing it in mathlib, let's see.

[Adrian Marti]

Yeah I asked ChatGPT which gave me the answer haha, but can we do this with loogle?

[Adrian Marti]

Darij Grinberg said:

i don't get loogle either, but searching for a word is probably the easiest way of using it :)

True

[Darij Grinberg]

how well does GPT speak lean4 by now?

[Adrian Marti]

I just asked it to browse the mathlib 4 docs, which it apparently can. But it can't browse zulip.

[Kenny Lau]

Adrian Marti said:

So let's say I want to extend a function Fin n -> X to a function Fin (n + 1) -> X given an a: X. Can I search this with loogle?

I did (Fin ?n → _) → (Fin (?n+1) → _) which didn't find it directly, but I did see Fin.cons and Fin.snoc mentioned, which are the functions you want, but they didn't show up because those are actually dependent functions, i.e. the return type is not constant

[Riccardo Brasca]

Yeah, I also just noticed the same

[Riccardo Brasca]

It's a bit unfortunate

[Adrian Marti]

I see the problem

[Kenny Lau]

setting them as dependent functions actually was successful, (∀ x : Fin ?n, ?a x) → (∀ x : Fin (?n + 1), ?a x) returns those two functions in addition to Fin.lastCases and Fin.cases!

[Kenny Lau]

and even more, it also reveals Fin.succAboveCases

[Kenny Lau]

i mean, what am i saying, all 10 of those results are valid

[Kenny Lau]

@Adrian Marti i hope this demonstrates to you the power of loogle :upside_down:

[Riccardo Brasca]

Does exact? work?

[Riccardo Brasca]

Or does it find like the constant function?

[Riccardo Brasca]

It finds the constant function :(

[Riccardo Brasca]

What is the syntax of exact? using?

[Adrian Marti]

Kenny Lau said:

Adrian Marti i hope this demonstrates to you the power of loogle :upside_down:

It's definitely something that can be explored :slight_smile: