O cálculo formal de Planos de Corte é uma técnica matemática utilizada na área de otimização, particularmente em Programação Linear. Neste trabalho, procuramos trazer essa lógica para os resultados formalizados em Lean 4, seguindo a tendência crescente no mundo da matemática e atendendo a necessidade de confiança nos resultados de solucionadores. Além da formalização, procuramos aqui disponibilizar estes resultados para a comunidade em geral, para que mais integrações entre projetos possam ser possíveis no futuro.