Connect with us


Charging a quantum battery with linear feedback control



Mark T. Mitchison1, John Goold1, and Javier Prior2,3

1School of Physics, Trinity College Dublin, College Green, Dublin 2, Ireland
2Departamento de Física Aplicada, Universidad Politécnica de Cartagena, Cartagena E-30202, Spain
3Instituto Carlos I de Física Teórica y Computacional, Universidad de Granada, Granada E-18071, Spain

Find this paper interesting or want to discuss? Scite or leave a comment on SciRate.


Energy storage is a basic physical process with many applications. When considering this task at the quantum scale, it becomes important to optimise the non-equilibrium dynamics of energy transfer to the storage device or battery. Here, we tackle this problem using the methods of quantum feedback control. Specifically, we study the deposition of energy into a quantum battery via an auxiliary charger. The latter is a driven-dissipative two-level system subjected to a homodyne measurement whose output signal is fed back linearly into the driving field amplitude. We explore two different control strategies, aiming to stabilise either populations or quantum coherences in the state of the charger. In both cases, linear feedback is shown to counteract the randomising influence of environmental noise and allow for stable and effective battery charging. We analyse the effect of realistic control imprecisions, demonstrating that this good performance survives inefficient measurements and small feedback delays. Our results highlight the potential of continuous feedback for the control of energetic quantities in the quantum regime.

Talk at International Workshop “Open Quantum Dynamics and Thermodynamics”, hosted by the Center for Theoretical Physics of Complex Systems, Institute for Basic Science, South Korea.

Quantum batteries are useful models to explore the fundamental limits of energy transduction using controlled quantum systems. Recent research has focused on the effect of noise from the battery’s environment on the charging process. Here, we introduce and explore a charging protocol based on quantum feedback control. Focussing our attention on a minimal model, we show that information gained through weak measurements on the environment can be exploited to reliably suppress noise and enhance the battery’s charging performance. Such control can be implemented in various platforms including electronic and optical systems, opening up interesting possibilities for the experimental manipulation of energetic quantities with continuous quantum feedback.

► BibTeX data

► References

[1] H. M. Wiseman and G. J. Milburn, Quantum Measurement and Control (Cambridge University Press, 2009).

[2] M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information (Cambridge University Press, Cambridge, 2010).

[3] A. Polkovnikov, K. Sengupta, A. Silva, and M. Vengalattore, Rev. Mod. Phys. 83, 863 (2011).

[4] F. Campaioli, F. A. Pollock, and S. Vinjanampathy, in Thermodynamics in the Quantum Regime, edited by F. Binder, L. Correa, C. Gogolin, J. Anders, and G. Adesso (Springer Nature, 2018) 1805.05507.

[5] S. Bhattacharjee and A. Dutta, arXiv:2008.07889 [quant-ph] (2020).

[6] A. E. Allahverdyan, R. Balian, and T. M. Nieuwenhuizen, Europhys. Lett. 67, 565 (2004).

[7] M. Esposito and C. van den Broeck, Europhys. Lett. 95, 40004 (2011).

[8] F. Brandão, M. Horodecki, N. Ng, J. Oppenheim, and S. Wehner, Proc. Nat. Acad. Sci. 112, 3275 (2015).

[9] E. G. Brown, N. Friis, and M. Huber, New J. Phys. 18, 113028 (2016).

[10] G. T. Landi and M. Paternostro, arXiv:2009.07668 [quant-ph] (2020).

[11] R. Alicki and M. Fannes, Phys. Rev. E 87, 042123 (2013).

[12] K. V. Hovhannisyan, M. Perarnau-Llobet, M. Huber, and A. Acín, Phys. Rev. Lett. 111, 240401 (2013).

[13] M. Perarnau-Llobet, K. V. Hovhannisyan, M. Huber, P. Skrzypczyk, N. Brunner, and A. Acín, Phys. Rev. X 5, 041011 (2015).

[14] G. L. Giorgi and S. Campbell, J. Phys. B: Atom. Mol. Opt. Phys. 48, 035501 (2015).

[15] K. Korzekwa, M. Lostaglio, J. Oppenheim, and D. Jennings, New J. Phys. 18, 023045 (2016).

[16] G. Francica, F. C. Binder, G. Guarnieri, M. T. Mitchison, J. Goold, and F. Plastina, Phys. Rev. Lett. 125, 180603 (2020).

[17] F. C. Binder, S. Vinjanampathy, K. Modi, and J. Goold, New J. Phys. 17, 075015 (2015a).

[18] F. Campaioli, F. A. Pollock, F. C. Binder, L. Céleri, J. Goold, S. Vinjanampathy, and K. Modi, Phys. Rev. Lett. 118, 150601 (2017).

[19] T. P. Le, J. Levinsen, K. Modi, M. M. Parish, and F. A. Pollock, Phys. Rev. A 97, 022106 (2018).

[20] G. M. Andolina, M. Keck, A. Mari, M. Campisi, V. Giovannetti, and M. Polini, Phys. Rev. Lett. 122, 047702 (2019a).

[21] G. M. Andolina, M. Keck, A. Mari, V. Giovannetti, and M. Polini, Phys. Rev. B 99, 205437 (2019b).

[22] D. Ferraro, G. M. Andolina, M. Campisi, V. Pellegrini, and M. Polini, Phys. Rev. B 100, 075433 (2019).

[23] D. Rosa, D. Rossini, G. M. Andolina, M. Polini, and M. Carrega, J. High Energy Phys. 2020, 67 (2020).

[24] Y.-Y. Zhang, T.-R. Yang, L. Fu, and X. Wang, Phys. Rev. E 99, 052106 (2019).

[25] F. Caravelli, G. Coulter-De Wit, L. P. García-Pintos, and A. Hamma, Phys. Rev. Research 2, 023095 (2020).

[26] S. Ghosh, T. Chanda, and A. Sen(De), Phys. Rev. A 101, 032115 (2020).

[27] D. Rossini, G. M. Andolina, D. Rosa, M. Carrega, and M. Polini, Phys. Rev. Lett. 125, 236402 (2020).

[28] F. H. Kamin, F. T. Tabesh, S. Salimi, and A. C. Santos, Phys. Rev. E 102, 052109 (2020a).

[29] S. Julià-Farré, T. Salamon, A. Riera, M. N. Bera, and M. Lewenstein, Phys. Rev. Research 2, 023113 (2020).

[30] D. Rossini, G. M. Andolina, and M. Polini, Phys. Rev. B 100, 115142 (2019).

[31] F. Pirmoradian and K. Mølmer, Phys. Rev. A 100, 043833 (2019).

[32] F. H. Kamin, F. T. Tabesh, S. Salimi, F. Kheirandish, and A. C. Santos, New J. Phys. 22, 083007 (2020b).

[33] M. Carrega, A. Crescente, D. Ferraro, and M. Sassetti, New J. Phys. 22, 083085 (2020).

[34] G. M. Andolina, D. Farina, A. Mari, V. Pellegrini, V. Giovannetti, and M. Polini, Phys. Rev. B 98, 205423 (2018).

[35] D. Ferraro, M. Campisi, G. M. Andolina, V. Pellegrini, and M. Polini, Phys. Rev. Lett. 120, 117702 (2018).

[36] D. Farina, G. M. Andolina, A. Mari, M. Polini, and V. Giovannetti, Phys. Rev. B 99, 035421 (2019).

[37] S. Gherardini, F. Campaioli, F. Caruso, and F. C. Binder, Phys. Rev. Research 2, 013095 (2020).

[38] A. C. Santos, B. Çakmak, S. Campbell, and N. T. Zinner, Phys. Rev. E 100, 032107 (2019).

[39] J. Q. Quach and W. J. Munro, Phys. Rev. Applied 14, 024092 (2020).

[40] F. Barra, Phys. Rev. Lett. 122, 210601 (2019).

[41] C. L. Latune, I. Sinayskiy, and F. Petruccione, Phys. Rev. A 99, 052105 (2019).

[42] K. V. Hovhannisyan, F. Barra, and A. Imparato, Phys. Rev. Research 2, 033413 (2020).

[43] B. Çakmak, Phys. Rev. E 102, 042111 (2020).

[44] F. T. Tabesh, F. H. Kamin, and S. Salimi, Phys. Rev. A 102, 052223 (2020).

[45] F. Tacchino, T. F. F. Santos, D. Gerace, M. Campisi, and M. F. Santos, Phys. Rev. E 102, 062133 (2020).

[46] A. C. Santos, A. Saguia, and M. S. Sarandy, Phys. Rev. E 101, 062114 (2020).

[47] H. F. Hofmann, G. Mahler, and O. Hess, Phys. Rev. A 57, 4877 (1998).

[48] J. Wang and H. M. Wiseman, Phys. Rev. A 64, 063810 (2001).

[49] R. Ruskov and A. N. Korotkov, Phys. Rev. B 66, 041401 (2002).

[50] T. L. Patti, A. Chantasri, L. P. García-Pintos, A. N. Jordan, and J. Dressel, Phys. Rev. A 96, 022311 (2017).

[51] V. Belavkin, in Information Complexity and Control in Quantum Physics (Springer Vienna, 1987) pp. 311–329.

[52] H. M. Wiseman and G. J. Milburn, Phys. Rev. Lett. 70, 548 (1993).

[53] A. N. Korotkov, Phys. Rev. B 60, 5737 (1999).

[54] A. Serafini, ISRN Optics 2012, 1 (2012).

[55] J. Zhang, Y.-x. Liu, R.-B. Wu, K. Jacobs, and F. Nori, Phys. Rep. 679, 1 (2017).

[56] J. M. Horowitz and K. Jacobs, Phys. Rev. Lett. 115, 130501 (2015).

[57] J. J. Alonso, E. Lutz, and A. Romito, Phys. Rev. Lett. 116, 080403 (2016).

[58] C. Elouard, D. A. Herrera-Martí, M. Clusel, and A. Auffèves, npj Quantum Inf. 3, 9 (2017).

[59] M. Naghiloo, D. Tan, P. M. Harrington, J. J. Alonso, E. Lutz, A. Romito, and K. W. Murch, Phys. Rev. Lett. 124, 110604 (2020).

[60] M. Debiossac, D. Grass, J. J. Alonso, E. Lutz, and N. Kiesel, Nature Commun. 11, 1360 (2020).

[61] M. T. Mitchison, M. P. Woods, J. Prior, and M. Huber, New J. Phys. 17, 115013 (2015).

[62] J. B. Brask and N. Brunner, Phys. Rev. E 92, 062101 (2015).

[63] S. Nimmrichter, J. Dai, A. Roulet, and V. Scarani, Quantum 1, 37 (2017).

[64] G. Maslennikov, S. Ding, R. Hablützel, J. Gan, A. Roulet, S. Nimmrichter, J. Dai, V. Scarani, and D. Matsukevich, Nature Commun. 10, 202 (2019).

[65] H. Carmichael, An Open Systems Approach to Quantum Optics (Springer Berlin Heidelberg, 1993).

[66] H. M. Wiseman, Phys. Rev. A 49, 2133 (1994).

[67] P. Bushev, D. Rotter, A. Wilson, F. Dubin, C. Becher, J. Eschner, R. Blatt, V. Steixner, P. Rabl, and P. Zoller, Phys. Rev. Lett. 96, 043003 (2006).

[68] F. Tebbenjohanns, M. Frimmer, A. Militaru, V. Jain, and L. Novotny, Phys. Rev. Lett. 122, 223601 (2019).

[69] G. P. Conangla, F. Ricci, M. T. Cuairan, A. W. Schell, N. Meyer, and R. Quidant, Phys. Rev. Lett. 122, 223602 (2019).

[70] R. Vijay, C. Macklin, D. H. Slichter, S. J. Weber, K. W. Murch, R. Naik, A. N. Korotkov, and I. Siddiqi, Nature 490, 77 (2012).

[71] E. Buks, R. Schuster, M. Heiblum, D. Mahalu, and V. Umansky, Nature 391, 871 (1998).

[72] H.-S. Goan, G. J. Milburn, H. M. Wiseman, and H. Bi Sun, Phys. Rev. B 63, 125326 (2001).

[73] W. Pusz and S. L. Woronowicz, Commun. Math. Phys. 58, 273 (1978).

[74] F. Binder, S. Vinjanampathy, K. Modi, and J. Goold, Phys. Rev. E 91, 032119 (2015b).

[75] N. Brunner, N. Linden, S. Popescu, and P. Skrzypczyk, Phys. Rev. E 85, 051117 (2012).

[76] P. Skrzypczyk, R. Silva, and N. Brunner, Phys. Rev. E 91, 052133 (2015).

[77] P. Rouchon and J. F. Ralph, Phys. Rev. A 91, 012118 (2015).

[78] A. C. Doherty and K. Jacobs, Phys. Rev. A 60, 2700 (1999).

[79] H. M. Wiseman, S. Mancini, and J. Wang, Phys. Rev. A 66, 013807 (2002).

[80] N. Friis and M. Huber, Quantum 2, 61 (2018).

[81] L. P. García-Pintos, A. Hamma, and A. del Campo, Phys. Rev. Lett. 125, 040601 (2020).

[82] A. Crescente, M. Carrega, M. Sassetti, and D. Ferraro, New J. Phys. 22, 063057 (2020).

[83] A. Rignon-Bret, G. Guarnieri, J. Goold, and M. T. Mitchison, Phys. Rev. E 103, 012133 (2021).

[84] J. Åberg, Nature Commun. 4, 1925 (2013).

[85] D. Egloff, O. C. O. Dahlsten, R. Renner, and V. Vedral, New J. Phys. 17, 073001 (2015).

[86] K. Abdelkhalek, Y. Nakata, and D. Reeb, arXiv:1609.06981 [quant-ph] (2016).

[87] P. Kammerlander and J. Anders, Sci. Rep. 6, 22174 (2016).

[88] C. Elouard and A. N. Jordan, Phys. Rev. Lett. 120, 260601 (2018).

[89] T. Debarba, G. Manzano, Y. Guryanova, M. Huber, and N. Friis, New J. Phys. 21, 113002 (2019).

[90] Y. Guryanova, N. Friis, and M. Huber, Quantum 4, 222 (2020).

[91] G. Schaller, C. Emary, G. Kiesslich, and T. Brandes, Phys. Rev. B 84, 085418 (2011).

[92] M. D. Vidrighin, O. Dahlsten, M. Barbieri, M. S. Kim, V. Vedral, and I. A. Walmsley, Phys. Rev. Lett. 116, 050401 (2016).

[93] N. Cottet, S. Jezouin, L. Bretheau, P. Campagne-Ibarcq, Q. Ficheux, J. Anders, A. Auffèves, R. Azouit, P. Rouchon, and B. Huard, Proc. Nat. Acad. Sci. 114, 7561 (2017).

[94] T. Sagawa and M. Ueda, Phys. Rev. Lett. 100, 080403 (2008).

[95] K. Jacobs, Phys. Rev. A 80, 012322 (2009).

[96] T. Sagawa and M. Ueda, Phys. Rev. Lett. 104, 090602 (2010).

[97] K. Jacobs, Phys. Rev. E 86, 040106 (2012).

[98] Z. Gong, Y. Ashida, and M. Ueda, Phys. Rev. A 94, 012107 (2016).

[99] M. Esposito and G. Schaller, Europhys. Lett. 99, 30003 (2012).

[100] P. Strasberg, G. Schaller, T. Brandes, and M. Esposito, Phys. Rev. Lett. 110, 040601 (2013a).

[101] P. Strasberg, G. Schaller, T. Brandes, and M. Esposito, Phys. Rev. E 88, 062107 (2013b).

[102] P. Strasberg, G. Schaller, T. Brandes, and M. Esposito, Phys. Rev. X 7, 021003 (2017).

[103] J. Dressel, A. Chantasri, A. N. Jordan, and A. N. Korotkov, Phys. Rev. Lett. 119, 220507 (2017).

[104] P. Strasberg, Phys. Rev. E 100, 022127 (2019).

[105] A. Belenchia, L. Mancino, G. T. Landi, and M. Paternostro, npj Quantum Inf. 6, 97 (2020).

[106] J. Monsel, M. Fellous-Asiani, B. Huard, and A. Auffèves, Phys. Rev. Lett. 124, 130601 (2020).

[107] M. T. Mitchison, Contemp. Physics 60, 164 (2019).

[108] S. Lloyd, Phys. Rev. A 62, 022108 (2000).

Cited by

[1] Junjie Liu and Dvira Segal, “Boosting quantum battery performance by structure engineering”, arXiv:2104.06522.

[2] Maria Maffei, Patrice A. Camati, and Alexia Auffèves, “Probing non-classical light fields with energetic witnesses in Waveguide Quantum Electro-Dynamics”, arXiv:2102.05941.

[3] Tathagata Karmakar, Philippe Lewalle, and Andrew N. Jordan, “Stochastic Path Integral Analysis of the Continuously Monitored Quantum Harmonic Oscillator”, arXiv:2103.06111.

[4] Stella Seah, Martí Perarnau-Llobet, Géraldine Haack, Nicolas Brunner, and Stefan Nimmrichter, “Quantum speed-up in collisional battery charging”, arXiv:2105.01863.

[5] Anna Delmonte, Alba Crescente, Matteo Carrega, Dario Ferraro, and Maura Sassetti, “Characterization of a Two-Photon Quantum Battery: Initial Conditions, Stability and Work Extraction”, Entropy 23 5, 612 (2021).

The above citations are from SAO/NASA ADS (last updated successfully 2021-07-13 14:59:26). The list may be incomplete as not all publishers provide suitable and complete citation data.

Could not fetch Crossref cited-by data during last attempt 2021-07-13 14:59:24: Could not fetch cited-by data for 10.22331/q-2021-07-13-500 from Crossref. This is normal if the DOI was registered recently.

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.
Click here to access.



Self-referenced hologram of a single photon beam



Quantum 5, 516 (2021).

Quantitative characterization of the spatial structure of single photons is essential for free-space quantum communication and quantum imaging. We introduce an interferometric technique that enables the complete characterization of a two-dimensional probability amplitude of a single photon. Importantly, in contrast to methods that use a reference photon for the phase measurement, our technique relies on a single photon interfering with itself. Our setup comprises of a heralded single-photon source with an unknown spatial phase and a modified Mach-Zehnder interferometer with a spatial filter in one of its arms. The spatial filter removes the unknown spatial phase and the filtered beam interferes with the unaltered beam passing through the other arm of the interferometer. We experimentally confirm the feasibility of our technique by reconstructing the spatial phase of heralded single photons using the lowest order interference fringes. This technique can be applied to the characterization of arbitrary pure spatial states of single photons.

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.
Click here to access.


Continue Reading


Causal influence in operational probabilistic theories



Quantum 5, 515 (2021).

We study the relation of causal influence between input systems of a reversible evolution and its output systems, in the context of operational probabilistic theories. We analyse two different definitions that are borrowed from the literature on quantum theory—where they are equivalent. One is the notion based on signalling, and the other one is the notion used to define the neighbourhood of a cell in a quantum cellular automaton. The latter definition, that we adopt in the general scenario, turns out to be strictly weaker than the former: it is possible for a system to have causal influence on another one without signalling to it. Remarkably, the counterexample comes from classical theory, where the proposed notion of causal influence determines a redefinition of the neighbourhood of a cell in cellular automata. We stress that, according to our definition, it is impossible anyway to have causal influence in the absence of an interaction, e.g. in a Bell-like scenario. We study various conditions for causal influence, and introduce the feature that we call $textit{no interaction without disturbance}$, under which we prove that signalling and causal influence coincide. The proposed definition has interesting consequences on the analysis of causal networks, and leads to a revision of the notion of neighbourhood for classical cellular automata, clarifying a puzzle regarding their quantisation that apparently makes the neighbourhood larger than the original one.

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.
Click here to access.


Continue Reading


On the distribution of the mean energy in the unitary orbit of quantum states



Quantum 5, 514 (2021).

Given a closed quantum system, the states that can be reached with a cyclic process are those with the same spectrum as the initial state. Here we prove that, under a very general assumption on the Hamiltonian, the distribution of the mean extractable work is very close to a gaussian with respect to the Haar measure. We derive bounds for both the moments of the distribution of the mean energy of the state and for its characteristic function, showing that the discrepancy with the normal distribution is increasingly suppressed for large dimensions of the system Hilbert space.

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.
Click here to access.


Continue Reading


Proof Assistant Makes Jump to Big-League Math



Computer proof assistants have been an intriguing subplot in mathematics for years — promising to automate core aspects of the way mathematicians work, but in practice having little effect on the field.

But a new result, completed in early June, has the feel of a rookie’s first hit in the big leagues: At last, a proof assistant has made a real contribution to the leading edge of mathematical research by verifying the correctness of a complicated, modern proof.

“It demonstrates that modern maths can be formalized in a theorem prover,” said Bhavik Mehta, a graduate student at the University of Cambridge who contributed to the work.

The proof in question is by Peter Scholze of the University of Bonn, one of the most widely respected mathematicians in the world. It is just one piece of a larger project called “condensed mathematics” that he and Dustin Clausen of the University of Copenhagen have been working on for several years.

Their goal is to create new foundations for topology, replacing the traditional notion of a topological space — whose examples include the sphere and the doughnut — with more versatile objects that the authors call condensed sets. In this new perspective, topological spaces are thought of as being assembled from infinite points of dust glued together.

That project includes a particularly important, difficult proof that Scholze worked out himself during a consuming week in July 2019. It establishes that an area of math called real functional analysis still works if you replace topological spaces with condensed sets.

Scholze began the proof on a Monday. He worked entirely in his head, barely writing anything down, let alone using a computer. By Thursday afternoon he’d nearly figured it out, save one piece that he just couldn’t get right. He was also feeling the strain of the intense concentration required to hold such a complicated argument in his active memory. So that night he unwound with some friends at a bar. He paid for it the next morning, Friday.

“I was completely hungover,” said Scholze.

But he also knew that he wouldn’t have time to work over the weekend, making Friday his best chance to finish the proof. The thought of losing touch with everything he’d built up in his mind over the past week, then having to start again fresh on Monday, was more than he wanted to consider.

“I didn’t think I’d have the mental capacity to rebuild this in my head again,” said Scholze.

So he powered through and finished the proof. But afterward, he wasn’t certain that what he had done was correct. The reason was more than the hazy circumstances in which he’d cleared the final hurdle. The proof was so complicated Scholze knew it was possible he had missed something.

“It’s some very convoluted thing with many moving parts. It’s hard to know which parts move by how much when you shift one of these parameters,” said Scholze.

Scholze didn’t find time to actually write down the proof until November 2019. A year later he contacted Kevin Buzzard, a mathematician at Imperial College London and a prominent evangelist for a proof assistant program called Lean. Scholze wanted to know whether it would be possible to type his proof into Lean — turning it into lines of code like a software program — so that the program could verify whether it was really true.

Buzzard shared Scholze’s inquiry with a handful of other members of the Lean community including Johan Commelin, a postdoctoral researcher at the University of Freiburg. Commelin had the perfect background for the job — he’d been using Lean for several years and was familiar with condensed mathematics — and he was convinced that verifying Scholze’s proof would do a lot to legitimize the proof assistant’s standing in the mathematical community.

“Being able to collaborate with Peter on such a project and having his name attached to it would be an enormous boost for Lean,” said Commelin.

But he also thought it could take a year or more to do it, which gave him pause. Commelin was worried he might spend all that time verifying the proof and, at the end, the rest of the math world would just shrug.

“I thought that if I spend two years working on this and I come out of my cave and say, ‘This is fine,’ the rest of the world is going to say, ‘Wow, we already knew this, Peter proved it,’” said Commelin. It wouldn’t matter that Scholze himself wasn’t entirely sure.

So Commelin asked Scholze if he’d be willing to make a public statement vouching for the importance of the work. Scholze agreed, and on Dec. 5, 2020, he wrote a post on Buzzard’s blog.

They called it the “Liquid Tensor Experiment,” a nod to mathematical objects involved in the proof called liquid real vector spaces, and to a progressive rock band he and Commelin enjoy called Liquid Tension Experiment. In the 4,400-word primer, Scholze explained some technical aspects of the result and then added a note testifying in plain language to what he saw as the importance of checking it with a computer.

“I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change,)” Scholze wrote. “Better be sure it’s correct…”

Assurance in place, Commelin set to work. After explaining to Lean the mathematical statement whose proof he ultimately wanted the program to check, he brought more mathematicians into the project. They identified a few lemmas — intermediate steps in the proof — that seemed most approachable. They formalized those first, coding them on top of the library of mathematical knowledge that Lean draws on to determine if a given statement is true or not.

Last October, Quanta wrote that the collective effort to write mathematics in Lean has the “air of a barn raising.” This project was no different. Commelin would identify discrete parts of the proof and post them to Zulip, a discussion board that serves as a hub for the Lean community. When mathematicians saw a part of the proof that fit their expertise, they’d volunteer to formalize it.

Mehta was one of about a dozen mathematicians who contributed to the work. In May he saw a post from Commelin asking for help formalizing the proof of a statement called Gordan’s lemma, which related to Mehta’s work in the area of combinatorial geometry. He spent a week coding the proof in terms that were consistent with the larger proof the mathematicians were building. It was emblematic, he said, of the way Lean works.

“It’s one big collaboration with a lot of people doing what they’re good at to make a singular monolith,” he said.

As the work proceeded, Scholze was a consistent presence on Zulip, answering questions and explaining points of the proof — a bit like an architect giving directions to builders on a job site. “He was always within reach,” Commelin said.

At the end of May the group finished formalizing the one part of the proof Scholze was most unsure about. Commelin entered the final keystroke at 1:10 a.m. on May 29. Lean compiled the proof, and it ran like a functioning program, verifying that Scholze’s work was 100% correct. Now Scholze and other mathematicians can apply those techniques from real functional analysis to condensed sets, knowing that they’ll definitely work in this new setting.

And while Scholze still prefers to work out proofs in his head, Lean’s abilities left him impressed. He can now foresee programs like it playing an enduring role in research mathematics.

“This experiment has changed drastically my impression of how capable [proof assistants] are,” Scholze said. “I now think it’s sensible in principle to formalize whatever you want in Lean. There’s no real obstruction.”

PlatoAi. Web3 Reimagined. Data Intelligence Amplified.

Click here to access.


Continue Reading
Ecommerce5 days ago

How professional videos can help e-commerce brands attract more customers

Blockchain3 days ago

Everything you should know about Coinbase

Blockchain1 day ago

CryptoHawk Provides Subscribers 2-month Returns of 44.5% on BTC and 22.1% on ETH

Cyber Security1 day ago

What is a Remote Access Code?

Gaming4 days ago

SCCG Management and Data Sports Group Partner to Deliver Sports Content and Analytics to the Media Industry

Startups1 day ago

From Red Gold to Olympic Gold: Seedo Corp. Seeks Solutions for Athletes and More

Gaming3 days ago

How to win the war on betting

Gaming3 days ago

How to master poker

Cleantech1 day ago

Why food production is as dangerous for the planet as fossil fuels

Blockchain1 day ago

Had Enough of Crypto? Here are Some Alternatives!

AR/VR1 day ago

nDreams Appoints ex Codemasters CEO as Non-Executive Chair of the Board

Blockchain1 day ago

GBA Names New United Kingdom Chapter President

Cleantech1 day ago

To sell EVs, are automakers ready to ditch dealerships?

AR/VR1 day ago

Ven VR Adventure Arrives on Oculus Quest Next Week

Cleantech1 day ago

Green bonds are beating all expectations in the post-pandemic recovery

Cleantech1 day ago

You’ve set a bold climate goal, so now what?

Blockchain1 day ago

From Around the Web: 10 Awesome Stories About Bitcoin

Blockchain2 days ago

Unique Network Chosen As Exclusive Blockchain Partner for United Nations Associated NFT Climate Initiative

Cyber Security2 days ago

What is Service Desk?

AR/VR2 days ago

The Walking Dead: Saints & Sinners Aftershocks Confirmed for Late September