feat(OEIS): conjecture relating A080170 and A051283

[Aditi0522]

Summary

This PR adds a formal conjecture relating the two OEIS sequences:

• A080170
• A051283

The conjecture formalizes the equivalence between the two characterizations described in the OEIS entries.

Context

This closes #1451.

Sources:

• https://oeis.org/A080170
• https://oeis.org/A051283

Details

• Added a new Lean file under FormalConjectures/Oeis/
• Includes an informal statement and a formal conjecture skeleton
• No existing PR was linked to this issue at the time of submission

Checklist

• Follows repository structure
• References the OEIS sources
• Does not modify existing conjectures

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[mo271]

Could we name the new file after only of the the sequences?

[eric-wieser]

I'm going to close this; it's clear to me that this was entirely authored with an LLM, as you have hallucinated syntax that doesn't exist (conjecture). If you aren't going to even spend the time to open this in Lean then our time would be better spent on other contributors.

[Aditi0522]

Hello all, I apologize if my current work has offended you all, I accept that I did take help from an LLM but it was not entirely authored by it. I was in process of running the build and correcting definitions on my local machine before adding new commits but it has taken some time since I am on windows. I would be immensely grateful if you can consider my request and reopen this PR, so I can address the issues properly and submit a corrected version.

It was not my intention to cause anyone any inconvenience, Thank you for your time and consideration.

[YaelDillies]

There you go, but next time please fix the build before you open a PR. Else we will ban you from further contributions.

[Aditi0522]

Thank you for considering my request! I understand where things went wrong on my side, and I’ll make sure to fully fix the build and validate everything locally before opening a new PR, so as not to waste anyone’s time.

I’ll submit a corrected version shortly and will carefully factcheck the definitions from my side. Thank you for your patience.

[Aditi0522]

@mo271 Alright, I will rename the file after OeisA080170, I wasn't sure before what to name the file as both sequences were related to one issue.

[eric-wieser]

There you go, but next time please fix the build before you open a PR.

Just to be clear; it's ok if there's something you can't work out how to fix and need advice for; just don't PR code without at least opening it in VSCode to check everything looks ok.

[Aditi0522]

Kindly review and let me know if there are any changes or updates I need to make.

[Aditi0522]

I’ve made the requested changes. Could you please take a look and let me know if the definitions are conceptually sound or if any further adjustments are needed? Thank you for your time.

[YaelDillies]

Thanks!