@alwayscurious@infosec.exchange @mei@donotsta.re one important thing to know about mathematics is that there are two layers to every problem: how to find the solution and how to formalize the solution. Finding the solution usually involves steps that are omitted when writing up the solution as a formal proof, but are just as important to develop. Oftentimes, the formal write-up ends up being the inverse of what you actually did to find the solution in the first place: you start out exploring your problem and noting necessary and sufficient conditions for it. Then you start looking at those conditions and try to find necessary and sufficient conditions for these etc. But when writing up the proof, you start with your collection of lemmas, and only move to prove the main theorem once you have all your preconditions sorted out. Reduction proofs follow a similar pattern: when actually doing the research, you don't start with "assuming I have an attack on my problem, how does this attack my building blocks", but you start with "what properties do I need and what building blocks provide those", and only when you have a construction that actually works you move to write it up as a formal reduction proof, following the breadcrumbs you got when constructing your protocol/primitive. The formal step is still very important, especially for primitives, as it ensures that nothing slipped through. In protocols you can use things like universal composability instead of reduction at times, making the proof look more natural.