Equivalencies for Prime Numbers?

Stream: Is there code for X?

[Jonatas Miguel]

What are some equivalencies for prime numbers that have been encoded in Lean? Are there any that are known to mathematics that haven't been encoded in Lean?

I tried looking via moogle.ai but, the way some of that stuff was expressed made me wonder if I was looking at equivalencies for prime numbers or some other objects that are called "prime".

[Riccardo Brasca]

Can you give an example of a statement you are looking for?

[Jonatas Miguel]

An equivalency that can break primes up into summative parts. Something like "for all q, q in Primes iff there exists a, b such that q = a + b and some-other-stuff"-ish.

[Riccardo Brasca]

It's difficult to answer without a precise statement. If you write a precise mathematical statement we can help finding it in the library, or proving it

[Jonatas Miguel]

Hmm, I suppose I misunderstood how searching would work. Is there no way to do a search with a portion of the thing we're trying to look for? I suppose I'm trying to search with only some of the statement because I assume that however I have the statement now it may not be expressed exactly that way elsewhere. At the very least I would expect the portion that I wrote above to be a part of whatever exists though. But, that's just an assumption from someone that hasn't worked on this stuff as extensively as others.

I appreciate your assistance @Riccardo Brasca but if I'm going to have to write out the full statement to search for it, I may just try to do the work in Lean myself at that point I think. I've been wanting to practice working with Lean more, and hopefully this would keep me motivated to do that.

[Riccardo Brasca]

I may be misunderstanding your goal. If you want to see characterisations of being prime you can use loogle and look for "prime", "iff"

[Riccardo Brasca]

It is surely possible to look for a partial statement, but we need more information to help

[Michael Stoll]

@loogle "prime", "iff"

[loogle]

:search: Nat.coprime_iff_gcd_eq_one, Nat.coprime_mul_iff_left, and 244 more

[Michael Stoll]

@loogle Nat.Prime, "iff"

[loogle]

:search: Nat.irreducible_iff_nat_prime, Nat.prime_iff, and 120 more

[Jonatas Miguel]

@Riccardo Brasca and @Michael Stoll thanks, that's what I was trying to look for. I wanted to know the different ways that primes have been expressed as equivalencies. I have one in mind and was wondering if it was already formalized or even part of mathematical literature. I'm looking through these search results now. Apologies if it felt like I was being difficult.

[Michael Stoll]

This is maybe more on target:
@loogle |- Nat.Prime _ <-> _

[loogle]

:search: Nat.prime_iff, Nat.prime_iff_prime_int, and 8 more

[Jonatas Miguel]

So, these searches would help tell me if what I'm looking for exists in Lean. I am aware that not every part of mathematics has been formalized with Lean. How do you then search mathematical literature for the same kind of thing? Are there tools that are publicly available to me that I could use to try to do this search?

[Jonatas Miguel]

Ok, so, just finished looking through those search results (thanks again for those), and it didn't seem like there was anything expressed like what I was searching for. I think I'll make an effort to formalize and prove in Lean the statement I have then. If it's a well known result within mathematics, I'm sure someone can notify me about that fact if/when I post that and I'll add credit where it's due.

[Mario Carneiro]

What are you searching for? It still sounds like you have more information than you are providing to the "search engine" here