Cayden

Stream: new members

[Cayden Codel]

Hi Lean Zulip community! My name is Cayden Codel, and I'm a current master's student at Carnegie Mellon University, co-advised by Dr. Jeremy Avigad and Dr. Marijn Heule. I've started to learn Lean this summer for my master's project. I'm looking forward to learning all about Lean!

[Kevin Buzzard]

What have they got you thinking about?

[Cayden Codel]

Right now, the plan is to use Lean to verify encodings of mathematical problems into propositional language/CNF for use in SAT solving

[Kevin Buzzard]

What class/classes of mathematical problems?

[Cayden Codel]

Mainly graph problems, I think. Simple graph coloring or perfect matching problems. Also, encoding methods. Often when you have a problem, you want to encode that at most one of a set of objects should be included in a solution, so At-Most-One encodings are needed. Proving that those accurately encode at most one is a challenge. XOR constraints are another popular one, and I think that's where I'll get started

[Cayden Codel]

So generally looking at more general methods of encoding rather than applications to any one problem, but we'll see where the research takes us

[li sheng]

SAT is a NPC problem ! It's interesting and challenging ! I think it's a good project to solve in lean !

[Wojciech Nawrocki]

Hi @Cayden Codel! Are you planning to use Lean 3 or Lean 4? For the latter, maybe Saturn is worth looking at.

[Cayden Codel]

Looks like it's worth a look. Thanks for the recommendation!