why is this answer so long? Why isn't it as follows. The conjugate prior of the Dirichellet is X. Saying what X says. Everything else is nice but makes it harder to extract the information people usually want to look up.

I think what confuses me the most right now is that discharging seems to place antecedents on the left of the proof line (|-) BUT that would imply P has been proved (or is an axiom), but we do NOT know that. Thus, it just seems very strange to me. How can we allow that without actually knowing if P is has been actually proved?

Also, what is "iow"?

this answer is difficult to understand. What does your notation "P1. Assume P" mean? Is there any meaning to the syntactic dot you put after P1? Is P1 a proposition? Or is it just outlining the steps of your informal reasoning?

hi Mirek, seems you're had to get in touch with. I was interested in getting in touch with u because of ur NIPS submission. Feel free to ping me at [email protected]

@darijgrinberg How would you suggest to search for this type of thing? I also feels like its a more unique type of research direction that its not clear if anyone is even really working on (maybe I'm wrong). But for me what would be awesome to see how to "implement" these intuitive heuristics (like Polya's volumes on it) on doing mathematics. A little less emphasize on the output being purely human-like but more emphasize on the "search algorithm" to be more human. Maybe it would automatically output human like proofs, but I find it fascinating how human mathematical creativity works.