New recruit

Stream: Quantum information

[sujan]

Hi I am new to lean as well as quantum computing. Hope to learn as I hope to do some things at their intersection

[Alex Meiburg]

Hi! Let us know if you're looking for pointers or places to help out. :)

[sujan]

i was thinking of working on formalizing grover's algorithm in lean. Can you please help me on what I should look at and how should I go through it

[sujan]

I am doing a course on quantum computing at my university and learning lean too

[Alex Meiburg]

That would be a great thing to do, yeah! There's a few different things that could be meant by "formalizing Grover's algorithm", of course. I think a good goal would be proving that the algorithm given in

https://en.wikipedia.org/wiki/Grover%27s_algorithm#Algorithm

has the given success probability. That is, you define that initial state, define the unitary operator U_omega that corresponds to a classical function with unique answer omega, and define the Grover diffusion operator as a unitary operator. Then the theorem would be that you get that

$\sin^2((r+1/2) \theta)$

success probability of getting omega when you measure in the classical basis.

[Alex Meiburg]

(Extensions would be showing that the the initial superposition, and the Grover diffusion operator, can be efficiently implemented in terms of standard gates; or generalizing the algorithm to where there are $k$ answers to $U_\omega$ instead of just the one. There's also the complementary bound that Grover's algorithm is essentially optimal for black-box oracles, which would be cool to have. These should all come later though!)

[sujan]

Thank you for the kind reply. Will start the work on it and keep on updating here

[Alex Meiburg]

Great, feel free to ask questions! Quantum computing and Lean are both a bit steep learning curves so I'm happy to help if you feel you're getting blocked on anything. :)

[sujan]

Could I ask you questions related to lean and quantum computing too if I get stuck anywhere??

[Alex Meiburg]

Sure, right in this channel is fine!