{"id":"palomar/PALOMAR-2026-08-27-000002","url":"https://github.com/BrandonMYates/csordas-comparator/tree/2b23c32b841044581b7fc7a2dca0df86255d490d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000002-v1.json","repo":"https://github.com/BrandonMYates/csordas-comparator","tags":["math.CA","math.CV","math.NT","msc:30D15","msc:26A51","msc:30D10","msc:11M06","complex-analysis","log-concavity","lean"],"score":0,"title":"BrandonMYates/csordas-comparator","trust":"high","domain":"math.CA","source":"palomar","authors":["Brandon Yates"],"reviews":0,"subject":"math.CA","summary":"This project formalizes in Lean 4 a counterexample to a log-concavity conjecture of Coffey and Csordas (Math. Comp. 82 (2013) 2265-2272, Conjecture 2.5, where the quantity below is written S_n), later restated as Open Problem 4.13 of Csordas (Comput. Methods Funct. Theory 15 (2015) 373-391). Let Phi be the kernel of Riemann's integral representation, Phi(u) = sum_{n>=1} (4 pi^2 n^4 e^{9u/2} - 6 pi n^2 e^{5u/2}) e^{-pi n^2 e^{2u}}, and set J_n(t) = (Phi^(n)(t))^2 - Phi^(n-1)(t) Phi^(n+1)(t), the n-th Laguerre expression of Phi. The conjecture asserts J_n(t) > 0 for every real t and every n >=…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"Two concavity problems for the Riemann kernel","identifier":"","relationship":"formalizes"}]}